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

comparison OD.agda @ 302:304c271b3d47

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
HOD and reduction mapping of Ordinals
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 28 Jun 2020 18:09:04 +0900
parents b012a915bbb5
children 7963b76df6e1
comparison
equal deleted inserted replaced
301:b012a915bbb5 302:304c271b3d47
65 -- ==→o≡ is necessary to prove axiom of extensionality. 65 -- ==→o≡ is necessary to prove axiom of extensionality.
66 -- 66 --
67 -- In classical Set Theory, sup is defined by Uion. Since we are working on constructive logic, 67 -- In classical Set Theory, sup is defined by Uion. Since we are working on constructive logic,
68 -- we need explict assumption on sup. 68 -- we need explict assumption on sup.
69 69
70 record HOD (odmax : Ordinal) : Set (suc n) where
71 field
72 hmax : {x : Ordinal } → x o< odmax
73 hdef : Ordinal → Set n
74
75 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
76 field
77 os→ : (x : Ordinal) → x o< maxordinal → Ordinal
78 os← : Ordinal → Ordinal
79 os←limit : (x : Ordinal) → os← x o< maxordinal
80 os-iso← : {x : Ordinal} → os→ (os← x) (os←limit x) ≡ x
81 os-iso→ : {x : Ordinal} → (lt : x o< maxordinal ) → os← (os→ x lt) ≡ x
82
83 open HOD
84
85 -- HOD→OD : {x : Ordinal} → HOD x → OD
86 -- HOD→OD hod = record { def = hdef {!!} }
87
70 record ODAxiom : Set (suc n) where 88 record ODAxiom : Set (suc n) where
71 -- OD can be iso to a subset of Ordinal ( by means of Godel Set ) 89 -- OD can be iso to a subset of Ordinal ( by means of Godel Set )
72 field 90 field
73 od→ord : OD → Ordinal 91 od→ord : OD → Ordinal
74 ord→od : Ordinal → OD 92 ord→od : Ordinal → OD
77 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x 95 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
78 ==→o≡ : { x y : OD } → (x == y) → x ≡ y 96 ==→o≡ : { x y : OD } → (x == y) → x ≡ y
79 -- supermum as Replacement Axiom ( corresponding Ordinal of OD has maximum ) 97 -- supermum as Replacement Axiom ( corresponding Ordinal of OD has maximum )
80 sup-o : ( OD → Ordinal ) → Ordinal 98 sup-o : ( OD → Ordinal ) → Ordinal
81 sup-o< : { ψ : OD → Ordinal } → ∀ {x : OD } → ψ x o< sup-o ψ 99 sup-o< : { ψ : OD → Ordinal } → ∀ {x : OD } → ψ x o< sup-o ψ
100 -- contra-position of mimimulity of supermum required in Power Set Axiom which we don't use
101 -- sup-x : {n : Level } → ( OD → Ordinal ) → Ordinal
102 -- sup-lb : {n : Level } → { ψ : OD → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
103
104 record HODAxiom : Set (suc n) where
105 -- OD can be iso to a subset of Ordinal ( by means of Godel Set )
106 field
107 mod : Ordinal
108 mod-limit : ¬ ((y : Ordinal) → mod ≡ osuc y)
109 os : OrdinalSubset mod
110 od→ord : HOD mod → Ordinal
111 ord→od : Ordinal → HOD mod
112 c<→o< : {x y : HOD mod } → hdef y (od→ord x) → od→ord x o< od→ord y
113 oiso : {x : HOD mod } → ord→od ( od→ord x ) ≡ x
114 diso : {x : Ordinal } → od→ord ( ord→od x ) ≡ x
115 ==→o≡ : { x y : OD } → (x == y) → x ≡ y
116 -- supermum as Replacement Axiom ( corresponding Ordinal of OD has maximum )
117 sup-o : ( HOD mod → Ordinal ) → Ordinal
118 sup-o< : { ψ : HOD mod → Ordinal } → ∀ {x : HOD mod } → ψ x o< sup-o ψ
82 -- contra-position of mimimulity of supermum required in Power Set Axiom which we don't use 119 -- contra-position of mimimulity of supermum required in Power Set Axiom which we don't use
83 -- sup-x : {n : Level } → ( OD → Ordinal ) → Ordinal 120 -- sup-x : {n : Level } → ( OD → Ordinal ) → Ordinal
84 -- sup-lb : {n : Level } → { ψ : OD → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) 121 -- sup-lb : {n : Level } → { ψ : OD → Ordinal } → {z : Ordinal } → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
85 122
86 postulate odAxiom : ODAxiom 123 postulate odAxiom : ODAxiom