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

comparison constructible-set.agda @ 16:ac362cc8b10f

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