Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison OD.agda @ 290:359402cc6c3d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
definition of filter
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 12 Jun 2020 19:19:16 +0900
parents d9d3654baee1
children ef93c56ad311
comparison
equal deleted inserted replaced
286:4ae48eed654a 290:359402cc6c3d
51 ⇔→== : { x y : OD } → ( {z : Ordinal } → def x z ⇔ def y z) → x == y 51 ⇔→== : { x y : OD } → ( {z : Ordinal } → def x z ⇔ def y z) → x == y
52 eq→ ( ⇔→== {x} {y} eq ) {z} m = proj1 eq m 52 eq→ ( ⇔→== {x} {y} eq ) {z} m = proj1 eq m
53 eq← ( ⇔→== {x} {y} eq ) {z} m = proj2 eq m 53 eq← ( ⇔→== {x} {y} eq ) {z} m = proj2 eq m
54 54
55 -- next assumptions are our axiom 55 -- next assumptions are our axiom
56 -- it defines a subset of OD, which is called HOD, usually defined as 56 -- In classical Set Theory, HOD is used, as a subset of OD,
57 -- HOD = { x | TC x ⊆ OD } 57 -- HOD = { x | TC x ⊆ OD }
58 -- where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x 58 -- where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x.
59 -- This is not possible because we don't have V yet.
60 -- We simply assume V=OD here.
61 --
62 -- We also assumes ODs are isomorphic to Ordinals, which is ususally proved by Goedel number tricks.
63 -- ODs have an ovbious maximum, but Ordinals are not. This means, od→ord is not an on-to mapping.
64 --
65 -- ==→o≡ is necessary to prove axiom of extensionality.
66 --
67 -- In classical Set Theory, sup is defined by Uion. Since we are working on constructive logic,
68 -- we need explict assumption on sup.
59 69
60 record ODAxiom : Set (suc n) where 70 record ODAxiom : Set (suc n) where
61 -- OD can be iso to a subset of Ordinal ( by means of Godel Set ) 71 -- OD can be iso to a subset of Ordinal ( by means of Godel Set )
62 field 72 field
63 od→ord : OD → Ordinal 73 od→ord : OD → Ordinal