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

comparison constructible-set.agda @ 22:3da2c00bd24d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
..
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 16 May 2019 17:20:45 +0900
parents 6d9fdd1dfa79
children 7293a151d949
comparison
equal deleted inserted replaced
21:6d9fdd1dfa79 22:3da2c00bd24d
36 open import Relation.Binary.Core 36 open import Relation.Binary.Core
37 37
38 o∅ : Ordinal 38 o∅ : Ordinal
39 o∅ = record { lv = Zero ; ord = Φ } 39 o∅ = record { lv = Zero ; ord = Φ }
40 40
41 TransFinite : ( ψ : Ordinal → Set n )
42 → ( ∀ (lx : Nat ) → ψ ( record { lv = Suc lx ; ord = ℵ lx } ))
43 → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ } ) )
44 → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc x } ) )
45 → ∀ (x : Ordinal) → ψ x
46 TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ } = caseΦ lv
47 TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc ord₁ } = caseOSuc lv ord₁
48 ( TransFinite ψ caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } ))
49 TransFinite ψ caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁
50
51 record SupR (ψ : Ordinal → Ordinal ) : Set n where
52 field
53 sup : Ordinal
54 smax : { x : Ordinal } → ψ x o< sup
55
56 open SupR
57
58 Sup : (ψ : Ordinal → Ordinal ) → SupR ψ
59 sup (Sup ψ) = {!!}
60 smax (Sup ψ) = {!!}
61
62 41
63 ≡→¬d< : {lv : Nat} → {x : OrdinalD lv } → x d< x → ⊥ 42 ≡→¬d< : {lv : Nat} → {x : OrdinalD lv } → x d< x → ⊥
64 ≡→¬d< {lx} {OSuc y} (s< t) = ≡→¬d< t 43 ≡→¬d< {lx} {OSuc y} (s< t) = ≡→¬d< t
65 44
66 trio<> : {lx : Nat} {x : OrdinalD lx } { y : OrdinalD lx } → y d< x → x d< y → ⊥ 45 trio<> : {lx : Nat} {x : OrdinalD lx } { y : OrdinalD lx } → y d< x → x d< y → ⊥
143 ; reflexive = case1 122 ; reflexive = case1
144 ; trans = OrdTrans 123 ; trans = OrdTrans
145 } 124 }
146 } 125 }
147 126
127 TransFinite : ( ψ : Ordinal → Set n )
128 → ( ∀ (lx : Nat ) → ψ ( record { lv = Suc lx ; ord = ℵ lx } ))
129 → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ } ) )
130 → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc x } ) )
131 → ∀ (x : Ordinal) → ψ x
132 TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ } = caseΦ lv
133 TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc ord₁ } = caseOSuc lv ord₁
134 ( TransFinite ψ caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } ))
135 TransFinite ψ caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁
136
137 record SupR (ψ : Ordinal → Ordinal ) : Set n where
138 field
139 sup : Ordinal
140 smax : { x : Ordinal } → ψ x o< sup
141
142 open SupR
143
144 Sup : (ψ : Ordinal → Ordinal ) → SupR ψ
145 sup (Sup ψ) = {!!}
146 smax (Sup ψ) = {!!}
147
148 -- X' = { x ∈ X | ψ x } ∪ X , Mα = ( ∪ (β < α) Mβ ) ' 148 -- X' = { x ∈ X | ψ x } ∪ X , Mα = ( ∪ (β < α) Mβ ) '
149 149
150 record ConstructibleSet : Set (suc (suc n)) where 150 record ConstructibleSet : Set (suc (suc n)) where
151 field 151 field
152 α : Ordinal 152 α : Ordinal