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

comparison constructible-set.agda @ 17:6a668c6086a5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 14 May 2019 13:52:19 +0900
parents ac362cc8b10f
children 627a79e61116
comparison
equal deleted inserted replaced
16:ac362cc8b10f 17:6a668c6086a5
5 5
6 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ) 6 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat )
7 7
8 open import Relation.Binary.PropositionalEquality 8 open import Relation.Binary.PropositionalEquality
9 9
10 data OridinalD : (lv : Nat) → Set n where 10 data OrdinalD : (lv : Nat) → Set n where
11 Φ : {lv : Nat} → OridinalD lv 11 Φ : {lv : Nat} → OrdinalD lv
12 OSuc : {lv : Nat} → OridinalD lv → OridinalD lv 12 OSuc : {lv : Nat} → OrdinalD lv → OrdinalD lv
13 ℵ_ : (lv : Nat) → OridinalD (Suc lv) 13 ℵ_ : (lv : Nat) → OrdinalD (Suc lv)
14 14
15 record Ordinal : Set n where 15 record Ordinal : Set n where
16 field 16 field
17 lv : Nat 17 lv : Nat
18 ord : OridinalD lv 18 ord : OrdinalD lv
19 19
20 data _o<_ : {lx ly : Nat} → OridinalD lx → OridinalD ly → Set n where 20 data _d<_ : {lx ly : Nat} → OrdinalD lx → OrdinalD ly → Set n where
21 l< : {lx ly : Nat } → {x : OridinalD lx } → {y : OridinalD ly } → lx < ly → x o< y 21 Φ< : {lx : Nat} → {x : OrdinalD lx} → Φ {lx} d< OSuc {lx} x
22 Φ< : {lx : Nat} → {x : OridinalD lx} → Φ {lx} o< OSuc {lx} x 22 s< : {lx : Nat} → {x y : OrdinalD lx} → x d< y → OSuc {lx} x d< OSuc {lx} y
23 s< : {lx : Nat} → {x y : OridinalD lx} → x o< y → OSuc {lx} x o< OSuc {lx} y 23 ℵΦ< : {lx : Nat} → {x : OrdinalD (Suc lx) } → Φ {Suc lx} d< (ℵ lx)
24 ℵΦ< : {lx : Nat} → {x : OridinalD (Suc lx) } → Φ {Suc lx} o< (ℵ lx) 24 ℵ< : {lx : Nat} → {x : OrdinalD (Suc lx) } → OSuc {Suc lx} x d< (ℵ lx)
25 ℵ< : {lx : Nat} → {x : OridinalD (Suc lx) } → OSuc {Suc lx} x o< (ℵ lx) 25
26 open Ordinal
27
28 _o<_ : ( x y : Ordinal ) → Set n
29 _o<_ x y = (lv x < lv y ) ∨ ( ord x d< ord y )
26 30
27 open import Data.Nat.Properties 31 open import Data.Nat.Properties
28 open import Data.Empty 32 open import Data.Empty
29 open import Relation.Nullary 33 open import Relation.Nullary
30 34
31 open import Relation.Binary 35 open import Relation.Binary
32 open import Relation.Binary.Core 36 open import Relation.Binary.Core
33 37
38 ≡→¬d< : {lv : Nat} → {x : OrdinalD lv } → x d< x → ⊥
39 ≡→¬d< {lx} {OSuc y} (s< t) = ≡→¬d< t
34 40
35 ≡→¬< : { x y : Nat } → x ≡ y → x < y → ⊥ 41 trio<> : {lx : Nat} {x : OrdinalD lx } { y : OrdinalD lx } → y d< x → x d< y → ⊥
36 ≡→¬< {Zero} {Zero} refl ()
37 ≡→¬< {Suc x} {.(Suc x)} refl (s≤s t) = ≡→¬< {x} {x} refl t
38
39 x≤x : { x : Nat } → x ≤ x
40 x≤x {Zero} = z≤n
41 x≤x {Suc x} = s≤s ( x≤x )
42
43 x<>y : { x y : Nat } → x > y → x < y → ⊥
44 x<>y {.(Suc _)} {.(Suc _)} (s≤s lt) (s≤s lt1) = x<>y lt lt1
45
46 triO> : {lx ly : Nat} {x : OridinalD lx } { y : OridinalD ly } → ly < lx → x o< y → ⊥
47 triO> {lx} {ly} {x} {y} y<x xo<y with <-cmp lx ly
48 triO> {lx} {ly} {x} {y} y<x xo<y | tri< a ¬b ¬c = ¬c y<x
49 triO> {lx} {ly} {x} {y} y<x xo<y | tri≈ ¬a b ¬c = ¬c y<x
50 triO> {lx} {ly} {x} {y} y<x (l< x₁) | tri> ¬a ¬b c = ¬a x₁
51 triO> {lx} {ly} {Φ} {OSuc _} y<x Φ< | tri> ¬a ¬b c = ¬b refl
52 triO> {lx} {ly} {OSuc px} {OSuc py} y<x (s< w) | tri> ¬a ¬b c = triO> y<x w
53 triO> {lx} {ly} {Φ {u}} {ℵ w} y<x ℵΦ< | tri> ¬a ¬b c = ¬b refl
54 triO> {lx} {ly} {(OSuc _)} {ℵ u} y<x ℵ< | tri> ¬a ¬b c = ¬b refl
55
56 ≡→¬o< : {lv : Nat} → {x : OridinalD lv } → x o< x → ⊥
57 ≡→¬o< {lx} {x} (l< y) = ≡→¬< refl y
58 ≡→¬o< {lx} {OSuc y} (s< t) = ≡→¬o< t
59
60 trio<> : {lx : Nat} {x : OridinalD lx } { y : OridinalD lx } → y o< x → x o< y → ⊥
61 trio<> {lx} {x} {y} (l< lt) _ = ≡→¬< refl lt
62 trio<> {lx} {x} {y} _ (l< lt) = ≡→¬< refl lt
63 trio<> {lx} {.(OSuc _)} {.(OSuc _)} (s< s) (s< t) = 42 trio<> {lx} {.(OSuc _)} {.(OSuc _)} (s< s) (s< t) =
64 trio<> s t 43 trio<> s t
65 44
66 trio<≡ : {lx : Nat} {x : OridinalD lx } { y : OridinalD lx } → x ≡ y → x o< y → ⊥ 45 trio<≡ : {lx : Nat} {x : OrdinalD lx } { y : OrdinalD lx } → x ≡ y → x d< y → ⊥
67 trio<≡ refl = ≡→¬o< 46 trio<≡ refl = ≡→¬d<
68 47
69 trio>≡ : {lx : Nat} {x : OridinalD lx } { y : OridinalD lx } → x ≡ y → y o< x → ⊥ 48 trio>≡ : {lx : Nat} {x : OrdinalD lx } { y : OrdinalD lx } → x ≡ y → y d< x → ⊥
70 trio>≡ refl = ≡→¬o< 49 trio>≡ refl = ≡→¬d<
71 50
72 triO : {lx ly : Nat} → OridinalD lx → OridinalD ly → Tri (lx < ly) ( lx ≡ ly ) ( lx > ly ) 51 triO : {lx ly : Nat} → OrdinalD lx → OrdinalD ly → Tri (lx < ly) ( lx ≡ ly ) ( lx > ly )
73 triO {lx} {ly} x y = <-cmp lx ly 52 triO {lx} {ly} x y = <-cmp lx ly
74 53
75 triOonSameLevel : {lx : Nat} → Trichotomous _≡_ ( _o<_ {lx} {lx} ) 54 triOrdd : {lx : Nat} → Trichotomous _≡_ ( _d<_ {lx} {lx} )
76 triOonSameLevel {lv} Φ Φ = tri≈ ≡→¬o< refl ≡→¬o< 55 triOrdd {lv} Φ Φ = tri≈ ≡→¬d< refl ≡→¬d<
77 triOonSameLevel {Suc lv} (ℵ lv) (ℵ lv) = tri≈ ≡→¬o< refl ≡→¬o< 56 triOrdd {Suc lv} (ℵ lv) (ℵ lv) = tri≈ ≡→¬d< refl ≡→¬d<
78 triOonSameLevel {lv} Φ (OSuc y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< ) 57 triOrdd {lv} Φ (OSuc y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< )
79 triOonSameLevel {.(Suc lv)} Φ (ℵ lv) = tri< (ℵΦ< {lv} {Φ} ) (λ ()) ( λ lt → trio<> lt ((ℵΦ< {lv} {Φ} )) ) 58 triOrdd {.(Suc lv)} Φ (ℵ lv) = tri< (ℵΦ< {lv} {Φ} ) (λ ()) ( λ lt → trio<> lt ((ℵΦ< {lv} {Φ} )) )
80 triOonSameLevel {Suc lv} (ℵ lv) Φ = tri> ( λ lt → trio<> lt (ℵΦ< {lv} {Φ} ) ) (λ ()) (ℵΦ< {lv} {Φ} ) 59 triOrdd {Suc lv} (ℵ lv) Φ = tri> ( λ lt → trio<> lt (ℵΦ< {lv} {Φ} ) ) (λ ()) (ℵΦ< {lv} {Φ} )
81 triOonSameLevel {Suc lv} (ℵ lv) (OSuc y) = tri> ( λ lt → trio<> lt (ℵ< {lv} {y} ) ) (λ ()) (ℵ< {lv} {y} ) 60 triOrdd {Suc lv} (ℵ lv) (OSuc y) = tri> ( λ lt → trio<> lt (ℵ< {lv} {y} ) ) (λ ()) (ℵ< {lv} {y} )
82 triOonSameLevel {lv} (OSuc x) Φ = tri> (λ lt → trio<> lt Φ<) (λ ()) Φ< 61 triOrdd {lv} (OSuc x) Φ = tri> (λ lt → trio<> lt Φ<) (λ ()) Φ<
83 triOonSameLevel {.(Suc lv)} (OSuc x) (ℵ lv) = tri< ℵ< (λ ()) (λ lt → trio<> lt ℵ< ) 62 triOrdd {.(Suc lv)} (OSuc x) (ℵ lv) = tri< ℵ< (λ ()) (λ lt → trio<> lt ℵ< )
84 triOonSameLevel {lv} (OSuc x) (OSuc y) with triOonSameLevel x y 63 triOrdd {lv} (OSuc x) (OSuc y) with triOrdd x y
85 triOonSameLevel {lv} (OSuc x) (OSuc y) | tri< a ¬b ¬c = tri< (s< a) (λ tx=ty → trio<≡ tx=ty (s< a) ) ( λ lt → trio<> lt (s< a) ) 64 triOrdd {lv} (OSuc x) (OSuc y) | tri< a ¬b ¬c = tri< (s< a) (λ tx=ty → trio<≡ tx=ty (s< a) ) ( λ lt → trio<> lt (s< a) )
86 triOonSameLevel {lv} (OSuc x) (OSuc x) | tri≈ ¬a refl ¬c = tri≈ ≡→¬o< refl ≡→¬o< 65 triOrdd {lv} (OSuc x) (OSuc x) | tri≈ ¬a refl ¬c = tri≈ ≡→¬d< refl ≡→¬d<
87 triOonSameLevel {lv} (OSuc x) (OSuc y) | tri> ¬a ¬b c = tri> ( λ lt → trio<> lt (s< c) ) (λ tx=ty → trio>≡ tx=ty (s< c) ) (s< c) 66 triOrdd {lv} (OSuc x) (OSuc y) | tri> ¬a ¬b c = tri> ( λ lt → trio<> lt (s< c) ) (λ tx=ty → trio>≡ tx=ty (s< c) ) (s< c)
88 67
89 <→≤ : {lx ly : Nat} → lx < ly → (Suc lx ≤ ly) 68 d<→lv : {x y : Ordinal } → ord x d< ord y → lv x ≡ lv y
90 <→≤ {Zero} {Suc ly} (s≤s lt) = s≤s z≤n 69 d<→lv Φ< = refl
91 <→≤ {Suc lx} {Zero} () 70 d<→lv (s< lt) = refl
92 <→≤ {Suc lx} {Suc ly} (s≤s lt) = s≤s (<→≤ lt) 71 d<→lv ℵΦ< = refl
72 d<→lv ℵ< = refl
93 73
94 orddtrans : {lx ly lz : Nat} {x : OridinalD lx } { y : OridinalD ly } { z : OridinalD lz } → x o< y → y o< z → x o< z 74 orddtrans : {lx : Nat} {x y z : OrdinalD lx } → x d< y → y d< z → x d< z
95 orddtrans {lx} {ly} {lz} x<y y<z with <-cmp lx ly | <-cmp ly lz 75 orddtrans {lx} {.Φ} {.(OSuc _)} {.(OSuc _)} Φ< (s< y<z) = Φ<
96 orddtrans {lx} {ly} {lz} x<y y<z | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = l< ( <-trans a a₁ ) 76 orddtrans {Suc lx} {Φ {Suc lx}} {OSuc y} {ℵ lx} Φ< ℵ< = ℵΦ< {lx} {y}
97 orddtrans {lx} {ly} {lz} x<y y<z | tri< a ¬b ¬c | tri≈ ¬a refl ¬c₁ = l< a 77 orddtrans {lx} {.(OSuc _)} {.(OSuc _)} {.(OSuc _)} (s< x<y) (s< y<z) = s< ( orddtrans x<y y<z )
98 orddtrans {lx} {ly} {lz} x<y y<z | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = l< {!!} -- ⊥-elim ( ¬a c ) 78 orddtrans {.(Suc _)} {.(OSuc _)} {.(OSuc _)} {.(ℵ _)} (s< x<y) ℵ< = ℵ<
99 orddtrans {lx} {ly} {lz} x<y y<z | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = l< {!!} 79 orddtrans {.(Suc _)} {.Φ} {.(ℵ _)} {z} ℵΦ< ()
100 orddtrans {lx} {ly} {lz} x<y y<z | tri> ¬a ¬b c | tri≈ ¬a₁ refl ¬c = l< {!!} 80 orddtrans {.(Suc _)} {.(OSuc _)} {.(ℵ _)} {z} ℵ< ()
101 orddtrans {lx} {ly} {lz} x<y y<z | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = {!!}
102 orddtrans {lx} {ly} {lz} x<y y<z | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = l< a
103 orddtrans {lx} {ly} {lz} x<y y<z | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = l< {!!}
104 orddtrans {lx} {lx} {lx} x<y y<z | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = orddtrans1 x<y y<z where
105 orddtrans1 : {lx : Nat} {x y z : OridinalD lx } → x o< y → y o< z → x o< z
106 orddtrans1 = {!!}
107
108
109 81
110 max : (x y : Nat) → Nat 82 max : (x y : Nat) → Nat
111 max Zero Zero = Zero 83 max Zero Zero = Zero
112 max Zero (Suc x) = (Suc x) 84 max Zero (Suc x) = (Suc x)
113 max (Suc x) Zero = (Suc x) 85 max (Suc x) Zero = (Suc x)
114 max (Suc x) (Suc y) = Suc ( max x y ) 86 max (Suc x) (Suc y) = Suc ( max x y )
115 87
116 -- use cannot use OridinalD (Data.Nat_⊔_ lx ly), I don't know why 88 maxαd : { lx : Nat } → OrdinalD lx → OrdinalD lx → OrdinalD lx
89 maxαd x y with triOrdd x y
90 maxαd x y | tri< a ¬b ¬c = y
91 maxαd x y | tri≈ ¬a b ¬c = x
92 maxαd x y | tri> ¬a ¬b c = x
117 93
118 maxα> : { lx ly : Nat } → OridinalD lx → OridinalD ly → lx > ly → OridinalD lx 94 maxα : Ordinal → Ordinal → Ordinal
119 maxα> x y _ = x 95 maxα x y with <-cmp (lv x) (lv y)
96 maxα x y | tri< a ¬b ¬c = x
97 maxα x y | tri> ¬a ¬b c = y
98 maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) }
120 99
121 maxα= : { lx : Nat } → OridinalD lx → OridinalD lx → OridinalD lx 100 OrdTrans : Transitive (λ ( a b : Ordinal ) → (a ≡ b) ∨ (Ordinal.lv a < Ordinal.lv b) ∨ (Ordinal.ord a d< Ordinal.ord b) )
122 maxα= x y with triOonSameLevel x y
123 maxα= x y | tri< a ¬b ¬c = y
124 maxα= x y | tri≈ ¬a b ¬c = x
125 maxα= x y | tri> ¬a ¬b c = x
126
127 OrdTrans : Transitive (λ ( a b : Ordinal ) → (a ≡ b) ∨ (Ordinal.lv a < Ordinal.lv b) ∨ (Ordinal.ord a o< Ordinal.ord b) )
128 OrdTrans (case1 refl) (case1 refl) = case1 refl 101 OrdTrans (case1 refl) (case1 refl) = case1 refl
129 OrdTrans (case1 refl) (case2 lt2) = case2 lt2 102 OrdTrans (case1 refl) (case2 lt2) = case2 lt2
130 OrdTrans (case2 lt1) (case1 refl) = case2 lt1 103 OrdTrans (case2 lt1) (case1 refl) = case2 lt1
131 OrdTrans (case2 (case1 x)) (case2 (case1 y)) = case2 ( case1 ( <-trans x y ) ) 104 OrdTrans (case2 (case1 x)) (case2 (case1 y)) = case2 (case1 ( <-trans x y ) )
132 OrdTrans (case2 (case1 x)) (case2 (case2 y)) = case2 {!!} 105 OrdTrans (case2 (case1 x)) (case2 (case2 y)) with d<→lv y
133 OrdTrans (case2 (case2 x)) (case2 (case1 y)) = case2 {!!} 106 OrdTrans (case2 (case1 x)) (case2 (case2 y)) | refl = case2 (case1 x )
134 OrdTrans (case2 (case2 x)) (case2 (case2 y)) = case2 {!!} 107 OrdTrans (case2 (case2 x)) (case2 (case1 y)) with d<→lv x
108 OrdTrans (case2 (case2 x)) (case2 (case1 y)) | refl = case2 (case1 y)
109 OrdTrans (case2 (case2 x)) (case2 (case2 y)) with d<→lv x | d<→lv y
110 OrdTrans (case2 (case2 x)) (case2 (case2 y)) | refl | refl = case2 (case2 (orddtrans x y ))
135 111
136 OrdPreorder : Preorder n n n 112 OrdPreorder : Preorder n n n
137 OrdPreorder = record { Carrier = Ordinal 113 OrdPreorder = record { Carrier = Ordinal
138 ; _≈_ = _≡_ 114 ; _≈_ = _≡_
139 ; _∼_ = λ a b → (a ≡ b) ∨ (Ordinal.lv a < Ordinal.lv b) ∨ (Ordinal.ord a o< Ordinal.ord b ) 115 ; _∼_ = λ a b → (a ≡ b) ∨ ( a o< b )
140 ; isPreorder = record { 116 ; isPreorder = record {
141 isEquivalence = record { refl = refl ; sym = sym ; trans = trans } 117 isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
142 ; reflexive = case1 118 ; reflexive = case1
143 ; trans = OrdTrans 119 ; trans = OrdTrans
144 } 120 }
145 } 121 }
146 122
147 -- X' = { x ∈ X | ψ x } ∪ X , Mα = ( ∪ (β < α) Mβ ) ' 123 -- X' = { x ∈ X | ψ x } ∪ X , Mα = ( ∪ (β < α) Mβ ) '
148 124
149 data Constructible {lv : Nat} ( α : OridinalD lv ) : Set (suc n) where 125 data Constructible ( α : Ordinal ) : Set (suc n) where
150 fsub : ( ψ : OridinalD lv → Set n ) → Constructible α 126 fsub : ( ψ : Ordinal → Set n ) → Constructible α
151 xself : OridinalD lv → Constructible α 127 xself : Ordinal → Constructible α
152 128
153 record ConstructibleSet : Set (suc n) where 129 record ConstructibleSet : Set (suc n) where
154 field 130 field
155 level : Nat 131 α : Ordinal
156 α : OridinalD level
157 constructible : Constructible α 132 constructible : Constructible α
158 133
159 open ConstructibleSet 134 open ConstructibleSet
160 135
161 data _c∋_ : {lv lv' : Nat} {α : OridinalD lv } {α' : OridinalD lv' } → 136 data _c∋_ : {α α' : Ordinal } →
162 Constructible {lv} α → Constructible {lv'} α' → Set n where 137 Constructible α → Constructible α' → Set n where
163 c> : {lv lv' : Nat} {α : OridinalD lv } {α' : OridinalD lv' } 138 c> : {α α' : Ordinal }
164 (ta : Constructible {lv} α ) ( tx : Constructible {lv'} α' ) → α' o< α → ta c∋ tx 139 (ta : Constructible α ) ( tx : Constructible α' ) → α' o< α → ta c∋ tx
165 xself-fsub : {lv : Nat} {α : OridinalD lv } 140 xself-fsub : {α : Ordinal }
166 (ta : OridinalD lv ) ( ψ : OridinalD lv → Set n ) → _c∋_ {_} {_} {α} {α} (xself ta ) ( fsub ψ) 141 (ta : Ordinal ) ( ψ : Ordinal → Set n ) → _c∋_ {α} {α} (xself ta ) ( fsub ψ)
167 fsub-fsub : {lv lv' : Nat} {α : OridinalD lv } 142 fsub-fsub : {α : Ordinal }
168 ( ψ : OridinalD lv → Set n ) ( ψ₁ : OridinalD lv → Set n ) → 143 ( ψ : Ordinal → Set n ) ( ψ₁ : Ordinal → Set n ) →
169 ( ∀ ( x : OridinalD lv ) → ψ x → ψ₁ x ) → _c∋_ {_} {_} {α} {α} ( fsub ψ ) ( fsub ψ₁) 144 ( ∀ ( x : Ordinal ) → ψ x → ψ₁ x ) → _c∋_ {α} {α} ( fsub ψ ) ( fsub ψ₁)
170 145
171 _∋_ : (ConstructibleSet ) → (ConstructibleSet ) → Set n 146 _∋_ : (ConstructibleSet ) → (ConstructibleSet ) → Set n
172 a ∋ x = constructible a c∋ constructible x 147 a ∋ x = constructible a c∋ constructible x
173 148
174 transitiveness : (a b c : ConstructibleSet ) → a ∋ b → b ∋ c → a ∋ c 149 -- transitiveness : (a b c : ConstructibleSet ) → a ∋ b → b ∋ c → a ∋ c
175 transitiveness a b c a∋b b∋c with constructible a c∋ constructible b | constructible b c∋ constructible c 150 -- transitiveness a b c a∋b b∋c with constructible a c∋ constructible b | constructible b c∋ constructible c
176 ... | t1 | t2 = {!!} 151 -- ... | t1 | t2 = {!!}
177 152
178 data _c≈_ : {lv lv' : Nat} {α : OridinalD lv } {α' : OridinalD lv' } → 153 data _c≈_ : {α α' : Ordinal} →
179 Constructible {lv} α → Constructible {lv'} α' → Set n where 154 Constructible α → Constructible α' → Set n where
180 crefl : {lv : Nat} {α : OridinalD lv } → _c≈_ {_} {_} {α} {α} (xself α ) (xself α ) 155 crefl : {α : Ordinal } → _c≈_ {α} {α} (xself α ) (xself α )
181 feq : {lv : Nat} {α : OridinalD lv } 156 feq : {lv : Nat} {α : Ordinal }
182 → ( ψ : OridinalD lv → Set n ) ( ψ₁ : OridinalD lv → Set n ) 157 → ( ψ : Ordinal → Set n ) ( ψ₁ : Ordinal → Set n )
183 → (∀ ( x : OridinalD lv ) → ψ x ⇔ ψ₁ x ) → _c≈_ {_} {_} {α} {α} ( fsub ψ ) ( fsub ψ₁) 158 → (∀ ( x : Ordinal ) → ψ x ⇔ ψ₁ x ) → _c≈_ {α} {α} ( fsub ψ ) ( fsub ψ₁)
184 159
185 _≈_ : (ConstructibleSet ) → (ConstructibleSet ) → Set n 160 _≈_ : (ConstructibleSet ) → (ConstructibleSet ) → Set n
186 a ≈ x = constructible a c≈ constructible x 161 a ≈ x = constructible a c≈ constructible x
187 162
188 ConstructibleSet→ZF : ZF {suc n} 163 ConstructibleSet→ZF : ZF {suc n}
189 ConstructibleSet→ZF = record { 164 ConstructibleSet→ZF = record {
190 ZFSet = ConstructibleSet 165 ZFSet = ConstructibleSet
191 ; _∋_ = _∋_ 166 ; _∋_ = _∋_
192 ; _≈_ = _≈_ 167 ; _≈_ = _≈_
193 ; ∅ = record { level = Zero ; α = Φ ; constructible = xself Φ } 168 ; ∅ = record { α = record {lv = Zero ; ord = Φ } ; constructible = xself ( record {lv = Zero ; ord = Φ }) }
194 ; _×_ = {!!} 169 ; _×_ = {!!}
195 ; Union = {!!} 170 ; Union = {!!}
196 ; Power = {!!} 171 ; Power = {!!}
197 ; Select = {!!} 172 ; Select = {!!}
198 ; Replace = {!!} 173 ; Replace = {!!}