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

comparison constructible-set.agda @ 24:3186bbee99dd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
separte level
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 18 May 2019 16:03:10 +0900
parents 7293a151d949
children 0f3d98e97593
comparison
equal deleted inserted replaced
23:7293a151d949 24:3186bbee99dd
1 open import Level 1 open import Level
2 module constructible-set (n : Level) where 2 module constructible-set where
3 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 ; _⊔_ to _n⊔_ ) 6 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
7 7
8 open import Relation.Binary.PropositionalEquality 8 open import Relation.Binary.PropositionalEquality
9 9
10 data OrdinalD : (lv : Nat) → Set n where 10 data OrdinalD {n : Level} : (lv : Nat) → Set n where
11 Φ : {lv : Nat} → OrdinalD lv 11 Φ : (lv : Nat) → OrdinalD lv
12 OSuc : {lv : Nat} → OrdinalD lv → OrdinalD lv 12 OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv
13 ℵ_ : (lv : Nat) → OrdinalD (Suc lv) 13 ℵ_ : (lv : Nat) → OrdinalD (Suc lv)
14 14
15 record Ordinal : Set n where 15 record Ordinal {n : Level} : Set n where
16 field 16 field
17 lv : Nat 17 lv : Nat
18 ord : OrdinalD lv 18 ord : OrdinalD {n} lv
19 19
20 data _d<_ : {lx ly : Nat} → OrdinalD lx → OrdinalD ly → Set n where 20 data _d<_ {n : Level} : {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Set n where
21 Φ< : {lx : Nat} → {x : OrdinalD lx} → Φ {lx} d< OSuc {lx} x 21 Φ< : {lx : Nat} → {x : OrdinalD {n} lx} → Φ lx d< OSuc lx x
22 s< : {lx : Nat} → {x y : OrdinalD lx} → x d< y → OSuc {lx} x d< OSuc {lx} y 22 s< : {lx : Nat} → {x y : OrdinalD {n} lx} → x d< y → OSuc lx x d< OSuc lx y
23 ℵΦ< : {lx : Nat} → {x : OrdinalD (Suc lx) } → Φ {Suc lx} d< (ℵ lx) 23 ℵΦ< : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } → Φ (Suc lx) d< (ℵ lx)
24 ℵ< : {lx : Nat} → {x : OrdinalD (Suc lx) } → OSuc {Suc lx} x d< (ℵ lx) 24 ℵ< : {lx : Nat} → {x : OrdinalD {n} (Suc lx) } → OSuc (Suc lx) x d< (ℵ lx)
25 25
26 open Ordinal 26 open Ordinal
27 27
28 _o<_ : ( x y : Ordinal ) → Set n 28 _o<_ : {n : Level} ( x y : Ordinal ) → Set (suc n)
29 _o<_ x y = (lv x < lv y ) ∨ ( ord x d< ord y ) 29 _o<_ x y = (lv x < lv y ) ∨ ( ord x d< ord y )
30 30
31 open import Data.Nat.Properties 31 open import Data.Nat.Properties
32 open import Data.Empty 32 open import Data.Empty
33 open import Relation.Nullary 33 open import Relation.Nullary
34 34
35 open import Relation.Binary 35 open import Relation.Binary
36 open import Relation.Binary.Core 36 open import Relation.Binary.Core
37 37
38 o∅ : Ordinal 38 o∅ : {n : Level} → Ordinal {n}
39 o∅ = record { lv = Zero ; ord = Φ } 39 o∅ = record { lv = Zero ; ord = Φ Zero }
40 40
41 41
42 ≡→¬d< : {lv : Nat} → {x : OrdinalD lv } → x d< x → ⊥ 42 ≡→¬d< : {n : Level} → {lv : Nat} → {x : OrdinalD {n} lv } → x d< x → ⊥
43 ≡→¬d< {lx} {OSuc y} (s< t) = ≡→¬d< t 43 ≡→¬d< {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t
44 44
45 trio<> : {lx : Nat} {x : OrdinalD lx } { y : OrdinalD lx } → y d< x → x d< y → ⊥ 45 trio<> : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → y d< x → x d< y → ⊥
46 trio<> {lx} {.(OSuc _)} {.(OSuc _)} (s< s) (s< t) = 46 trio<> {n} {lx} {.(OSuc lx _)} {.(OSuc lx _)} (s< s) (s< t) =
47 trio<> s t 47 trio<> s t
48 48
49 trio<≡ : {lx : Nat} {x : OrdinalD lx } { y : OrdinalD lx } → x ≡ y → x d< y → ⊥ 49 trio<≡ : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → x ≡ y → x d< y → ⊥
50 trio<≡ refl = ≡→¬d< 50 trio<≡ refl = ≡→¬d<
51 51
52 trio>≡ : {lx : Nat} {x : OrdinalD lx } { y : OrdinalD lx } → x ≡ y → y d< x → ⊥ 52 trio>≡ : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → x ≡ y → y d< x → ⊥
53 trio>≡ refl = ≡→¬d< 53 trio>≡ refl = ≡→¬d<
54 54
55 triO : {lx ly : Nat} → OrdinalD lx → OrdinalD ly → Tri (lx < ly) ( lx ≡ ly ) ( lx > ly ) 55 triO : {n : Level} → {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Tri (lx < ly) ( lx ≡ ly ) ( lx > ly )
56 triO {lx} {ly} x y = <-cmp lx ly 56 triO {n} {lx} {ly} x y = <-cmp lx ly
57 57
58 triOrdd : {lx : Nat} → Trichotomous _≡_ ( _d<_ {lx} {lx} ) 58 triOrdd : {n : Level} → {lx : Nat} → Trichotomous _≡_ ( _d<_ {n} {lx} {lx} )
59 triOrdd {lv} Φ Φ = tri≈ ≡→¬d< refl ≡→¬d< 59 triOrdd {_} {lv} (Φ lv) (Φ lv) = tri≈ ≡→¬d< refl ≡→¬d<
60 triOrdd {Suc lv} (ℵ lv) (ℵ lv) = tri≈ ≡→¬d< refl ≡→¬d< 60 triOrdd {_} {Suc lv} (ℵ lv) (ℵ lv) = tri≈ ≡→¬d< refl ≡→¬d<
61 triOrdd {lv} Φ (OSuc y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< ) 61 triOrdd {_} {lv} (Φ lv) (OSuc lv y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< )
62 triOrdd {.(Suc lv)} Φ (ℵ lv) = tri< (ℵΦ< {lv} {Φ} ) (λ ()) ( λ lt → trio<> lt ((ℵΦ< {lv} {Φ} )) ) 62 triOrdd {_} {.(Suc lv)} (Φ (Suc lv)) (ℵ lv) = tri< (ℵΦ< {_} {lv} {Φ (Suc lv)} ) (λ ()) ( λ lt → trio<> lt ((ℵΦ< {_} {lv} {Φ (Suc lv)} )) )
63 triOrdd {Suc lv} (ℵ lv) Φ = tri> ( λ lt → trio<> lt (ℵΦ< {lv} {Φ} ) ) (λ ()) (ℵΦ< {lv} {Φ} ) 63 triOrdd {_} {Suc lv} (ℵ lv) (Φ (Suc lv)) = tri> ( λ lt → trio<> lt (ℵΦ< {_} {lv} {Φ (Suc lv)} ) ) (λ ()) (ℵΦ< {_} {lv} {Φ (Suc lv)} )
64 triOrdd {Suc lv} (ℵ lv) (OSuc y) = tri> ( λ lt → trio<> lt (ℵ< {lv} {y} ) ) (λ ()) (ℵ< {lv} {y} ) 64 triOrdd {_} {Suc lv} (ℵ lv) (OSuc (Suc lv) y) = tri> ( λ lt → trio<> lt (ℵ< {_} {lv} {y} ) ) (λ ()) (ℵ< {_} {lv} {y} )
65 triOrdd {lv} (OSuc x) Φ = tri> (λ lt → trio<> lt Φ<) (λ ()) Φ< 65 triOrdd {_} {lv} (OSuc lv x) (Φ lv) = tri> (λ lt → trio<> lt Φ<) (λ ()) Φ<
66 triOrdd {.(Suc lv)} (OSuc x) (ℵ lv) = tri< ℵ< (λ ()) (λ lt → trio<> lt ℵ< ) 66 triOrdd {_} {.(Suc lv)} (OSuc (Suc lv) x) (ℵ lv) = tri< ℵ< (λ ()) (λ lt → trio<> lt ℵ< )
67 triOrdd {lv} (OSuc x) (OSuc y) with triOrdd x y 67 triOrdd {_} {lv} (OSuc lv x) (OSuc lv y) with triOrdd x y
68 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) ) 68 triOrdd {_} {lv} (OSuc lv x) (OSuc lv y) | tri< a ¬b ¬c = tri< (s< a) (λ tx=ty → trio<≡ tx=ty (s< a) ) ( λ lt → trio<> lt (s< a) )
69 triOrdd {lv} (OSuc x) (OSuc x) | tri≈ ¬a refl ¬c = tri≈ ≡→¬d< refl ≡→¬d< 69 triOrdd {_} {lv} (OSuc lv x) (OSuc lv x) | tri≈ ¬a refl ¬c = tri≈ ≡→¬d< refl ≡→¬d<
70 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) 70 triOrdd {_} {lv} (OSuc lv x) (OSuc lv y) | tri> ¬a ¬b c = tri> ( λ lt → trio<> lt (s< c) ) (λ tx=ty → trio>≡ tx=ty (s< c) ) (s< c)
71 71
72 d<→lv : {x y : Ordinal } → ord x d< ord y → lv x ≡ lv y 72 d<→lv : {n : Level} {x y : Ordinal {n}} → ord x d< ord y → lv x ≡ lv y
73 d<→lv Φ< = refl 73 d<→lv Φ< = refl
74 d<→lv (s< lt) = refl 74 d<→lv (s< lt) = refl
75 d<→lv ℵΦ< = refl 75 d<→lv ℵΦ< = refl
76 d<→lv ℵ< = refl 76 d<→lv ℵ< = refl
77 77
78 orddtrans : {lx : Nat} {x y z : OrdinalD lx } → x d< y → y d< z → x d< z 78 orddtrans : {n : Level} {lx : Nat} {x y z : OrdinalD {n} lx } → x d< y → y d< z → x d< z
79 orddtrans {lx} {.Φ} {.(OSuc _)} {.(OSuc _)} Φ< (s< y<z) = Φ< 79 orddtrans {_} {lx} {.(Φ lx)} {.(OSuc lx _)} {.(OSuc lx _)} Φ< (s< y<z) = Φ<
80 orddtrans {Suc lx} {Φ {Suc lx}} {OSuc y} {ℵ lx} Φ< ℵ< = ℵΦ< {lx} {y} 80 orddtrans {_} {Suc lx} {Φ (Suc lx)} {OSuc (Suc lx) y} {ℵ lx} Φ< ℵ< = ℵΦ< {_} {lx} {y}
81 orddtrans {lx} {.(OSuc _)} {.(OSuc _)} {.(OSuc _)} (s< x<y) (s< y<z) = s< ( orddtrans x<y y<z ) 81 orddtrans {_} {lx} {.(OSuc lx _)} {.(OSuc lx _)} {.(OSuc lx _)} (s< x<y) (s< y<z) = s< ( orddtrans x<y y<z )
82 orddtrans {.(Suc _)} {.(OSuc _)} {.(OSuc _)} {.(ℵ _)} (s< x<y) ℵ< = ℵ< 82 orddtrans {_} {Suc lx} {.(OSuc (Suc lx) _)} {.(OSuc (Suc lx) _)} {.(ℵ _)} (s< x<y) ℵ< = ℵ<
83 orddtrans {.(Suc _)} {.Φ} {.(ℵ _)} {z} ℵΦ< () 83 orddtrans {_} {Suc lx} {Φ (Suc lx)} {.(ℵ _)} {z} ℵΦ< ()
84 orddtrans {.(Suc _)} {.(OSuc _)} {.(ℵ _)} {z} ℵ< () 84 orddtrans {_} {Suc lx} {OSuc (Suc lx) _} {.(ℵ _)} {z} ℵ< ()
85 85
86 max : (x y : Nat) → Nat 86 max : (x y : Nat) → Nat
87 max Zero Zero = Zero 87 max Zero Zero = Zero
88 max Zero (Suc x) = (Suc x) 88 max Zero (Suc x) = (Suc x)
89 max (Suc x) Zero = (Suc x) 89 max (Suc x) Zero = (Suc x)
90 max (Suc x) (Suc y) = Suc ( max x y ) 90 max (Suc x) (Suc y) = Suc ( max x y )
91 91
92 maxαd : { lx : Nat } → OrdinalD lx → OrdinalD lx → OrdinalD lx 92 maxαd : {n : Level} → { lx : Nat } → OrdinalD {n} lx → OrdinalD lx → OrdinalD lx
93 maxαd x y with triOrdd x y 93 maxαd x y with triOrdd x y
94 maxαd x y | tri< a ¬b ¬c = y 94 maxαd x y | tri< a ¬b ¬c = y
95 maxαd x y | tri≈ ¬a b ¬c = x 95 maxαd x y | tri≈ ¬a b ¬c = x
96 maxαd x y | tri> ¬a ¬b c = x 96 maxαd x y | tri> ¬a ¬b c = x
97 97
98 maxα : Ordinal → Ordinal → Ordinal 98 maxα : {n : Level} → Ordinal {n} → Ordinal → Ordinal
99 maxα x y with <-cmp (lv x) (lv y) 99 maxα x y with <-cmp (lv x) (lv y)
100 maxα x y | tri< a ¬b ¬c = x 100 maxα x y | tri< a ¬b ¬c = x
101 maxα x y | tri> ¬a ¬b c = y 101 maxα x y | tri> ¬a ¬b c = y
102 maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) } 102 maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) }
103 103
104 _o≤_ : Ordinal → Ordinal → Set n 104 _o≤_ : {n : Level} → Ordinal → Ordinal → Set (suc n)
105 a o≤ b = (a ≡ b) ∨ ( a o< b ) 105 a o≤ b = (a ≡ b) ∨ ( a o< b )
106 106
107 trio< : Trichotomous _≡_ _o<_ 107 trio< : {n : Level } → Trichotomous {suc n} _≡_ _o<_
108 trio< a b with <-cmp (lv a) (lv b) 108 trio< a b with <-cmp (lv a) (lv b)
109 trio< a b | tri< a₁ ¬b ¬c = tri< (case1 a₁) (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) {!!} 109 trio< a b | tri< a₁ ¬b ¬c = tri< (case1 a₁) (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) lemma1 where
110 trio< a b | tri> ¬a ¬b c = tri> {!!} (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) (case1 c) 110 lemma1 : ¬ (Suc (lv b) ≤ lv a) ∨ (ord b d< ord a)
111 lemma1 (case1 x) = ¬c x
112 lemma1 (case2 x) with d<→lv x
113 lemma1 (case2 x) | refl = ¬b refl
114 trio< a b | tri> ¬a ¬b c = tri> lemma1 (λ refl → ¬b (cong ( λ x → lv x ) refl ) ) (case1 c) where
115 lemma1 : ¬ (Suc (lv a) ≤ lv b) ∨ (ord a d< ord b)
116 lemma1 (case1 x) = ¬a x
117 lemma1 (case2 x) with d<→lv x
118 lemma1 (case2 x) | refl = ¬b refl
111 trio< a b | tri≈ ¬a refl ¬c with triOrdd ( ord a ) ( ord b ) 119 trio< a b | tri≈ ¬a refl ¬c with triOrdd ( ord a ) ( ord b )
112 trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = tri< (case2 a) (λ refl → ¬b {!!} ) {!!} 120 trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = tri< (case2 a) (λ refl → ¬b (lemma1 refl )) lemma2 where
113 trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = tri≈ {!!} refl {!!} 121 lemma1 : (record { lv = _ ; ord = x }) ≡ b → x ≡ ord b
114 trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = tri> {!!} {!!} (case2 c) 122 lemma1 refl = refl
115 123 lemma2 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< x)
116 OrdTrans : Transitive _o≤_ 124 lemma2 (case1 x) = ¬a x
125 lemma2 (case2 x) = trio<> x a
126 trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = tri> lemma2 (λ refl → ¬b (lemma1 refl )) (case2 c) where
127 lemma1 : (record { lv = _ ; ord = x }) ≡ b → x ≡ ord b
128 lemma1 refl = refl
129 lemma2 : ¬ (Suc (lv b) ≤ lv b) ∨ (x d< ord b)
130 lemma2 (case1 x) = ¬a x
131 lemma2 (case2 x) = trio<> x c
132 trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = tri≈ lemma1 refl lemma1 where
133 lemma1 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< ord b)
134 lemma1 (case1 x) = ¬a x
135 lemma1 (case2 x) = ≡→¬d< x
136
137 OrdTrans : {n : Level} → Transitive {suc n} _o≤_
117 OrdTrans (case1 refl) (case1 refl) = case1 refl 138 OrdTrans (case1 refl) (case1 refl) = case1 refl
118 OrdTrans (case1 refl) (case2 lt2) = case2 lt2 139 OrdTrans (case1 refl) (case2 lt2) = case2 lt2
119 OrdTrans (case2 lt1) (case1 refl) = case2 lt1 140 OrdTrans (case2 lt1) (case1 refl) = case2 lt1
120 OrdTrans (case2 (case1 x)) (case2 (case1 y)) = case2 (case1 ( <-trans x y ) ) 141 OrdTrans (case2 (case1 x)) (case2 (case1 y)) = case2 (case1 ( <-trans x y ) )
121 OrdTrans (case2 (case1 x)) (case2 (case2 y)) with d<→lv y 142 OrdTrans (case2 (case1 x)) (case2 (case2 y)) with d<→lv y
123 OrdTrans (case2 (case2 x)) (case2 (case1 y)) with d<→lv x 144 OrdTrans (case2 (case2 x)) (case2 (case1 y)) with d<→lv x
124 OrdTrans (case2 (case2 x)) (case2 (case1 y)) | refl = case2 (case1 y) 145 OrdTrans (case2 (case2 x)) (case2 (case1 y)) | refl = case2 (case1 y)
125 OrdTrans (case2 (case2 x)) (case2 (case2 y)) with d<→lv x | d<→lv y 146 OrdTrans (case2 (case2 x)) (case2 (case2 y)) with d<→lv x | d<→lv y
126 OrdTrans (case2 (case2 x)) (case2 (case2 y)) | refl | refl = case2 (case2 (orddtrans x y )) 147 OrdTrans (case2 (case2 x)) (case2 (case2 y)) | refl | refl = case2 (case2 (orddtrans x y ))
127 148
128 OrdPreorder : Preorder n n n 149 OrdPreorder : {n : Level} → Preorder (suc n) (suc n) (suc n)
129 OrdPreorder = record { Carrier = Ordinal 150 OrdPreorder {n} = record { Carrier = Ordinal
130 ; _≈_ = _≡_ 151 ; _≈_ = _≡_
131 ; _∼_ = _o≤_ 152 ; _∼_ = _o≤_
132 ; isPreorder = record { 153 ; isPreorder = record {
133 isEquivalence = record { refl = refl ; sym = sym ; trans = trans } 154 isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
134 ; reflexive = case1 155 ; reflexive = case1
135 ; trans = OrdTrans 156 ; trans = OrdTrans
136 } 157 }
137 } 158 }
138 159
139 TransFinite : ( ψ : Ordinal → Set n ) 160 TransFinite : {n : Level} → ( ψ : Ordinal {n} → Set n )
140 → ( ∀ (lx : Nat ) → ψ ( record { lv = Suc lx ; ord = ℵ lx } )) 161 → ( ∀ (lx : Nat ) → ψ ( record { lv = Suc lx ; ord = ℵ lx } ))
141 → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ } ) ) 162 → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ lx } ) )
142 → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc x } ) ) 163 → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) )
143 → ∀ (x : Ordinal) → ψ x 164 → ∀ (x : Ordinal) → ψ x
144 TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ } = caseΦ lv 165 TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ lv } = caseΦ lv
145 TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc ord₁ } = caseOSuc lv ord₁ 166 TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc lv ord₁ } = caseOSuc lv ord₁
146 ( TransFinite ψ caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } )) 167 ( TransFinite ψ caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } ))
147 TransFinite ψ caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁ 168 TransFinite ψ caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁
148 169
149 -- X' = { x ∈ X | ψ x } ∪ X , Mα = ( ∪ (β < α) Mβ ) ' 170 -- X' = { x ∈ X | ψ x } ∪ X , Mα = ( ∪ (β < α) Mβ ) '
150 171
151 record ConstructibleSet : Set (suc (suc n)) where 172 record ConstructibleSet {n : Level} : Set (suc n) where
152 field 173 field
153 α : Ordinal 174 α : Ordinal {suc n}
154 constructible : Ordinal → Set (suc n) 175 constructible : Ordinal {suc n} → Set n
155 176
156 open ConstructibleSet 177 open ConstructibleSet
157 178
158 _∋_ : (ConstructibleSet ) → (ConstructibleSet ) → Set (suc n) 179 _∋_ : {n : Level} → (ConstructibleSet {n}) → (ConstructibleSet {n} ) → Set (suc n)
159 a ∋ x = ( α x o< α a ) ∧ constructible a ( α x ) 180 a ∋ x = ( α x o< α a ) ∧ constructible a ( α x )
160 181
161 c∅ : ConstructibleSet 182 c∅ : {n : Level} → ConstructibleSet
162 c∅ = record {α = o∅ ; constructible = λ x → Lift (suc n) ⊥ } 183 c∅ {n} = record {α = o∅ ; constructible = λ x → Lift n ⊥ }
163 184
164 record SupR {n m : Level} {S : Set n} ( _≤_ : S → S → Set m ) (ψ : S → S ) (X : S) : Set (n ⊔ m) where 185 record SupR {n m : Level} {S : Set n} ( _≤_ : S → S → Set m ) (ψ : S → S ) (X : S) : Set (n ⊔ m) where
165 field 186 field
166 sup : S 187 sup : S
167 smax : ∀ { x : S } → x ≤ X → ψ x ≤ sup 188 smax : ∀ { x : S } → x ≤ X → ψ x ≤ sup
168 suniq : {max : S} → ( ∀ { x : S } → x ≤ X → ψ x ≤ max ) → max ≤ sup 189 suniq : {max : S} → ( ∀ { x : S } → x ≤ X → ψ x ≤ max ) → max ≤ sup
169 190
170 open SupR 191 open SupR
171 192
172 _⊆_ : ( A B : ConstructibleSet ) → ∀{ x : ConstructibleSet } → Set (suc n) 193 _⊆_ : {n : Level} → ( A B : ConstructibleSet ) → ∀{ x : ConstructibleSet } → Set (suc n)
173 _⊆_ A B {x} = A ∋ x → B ∋ x 194 _⊆_ A B {x} = A ∋ x → B ∋ x
174 195
175 suptraverse : (X : ConstructibleSet ) ( max : ConstructibleSet) ( ψ : ConstructibleSet → ConstructibleSet ) → ConstructibleSet 196 suptraverse : {n : Level} → (X : ConstructibleSet {n}) ( max : ConstructibleSet {n}) ( ψ : ConstructibleSet {n} → ConstructibleSet {n}) → ConstructibleSet {n}
176 suptraverse X max ψ = {!!} 197 suptraverse X max ψ = {!!}
177 198
178 Sup : (ψ : ConstructibleSet → ConstructibleSet ) → (X : ConstructibleSet) → SupR (λ x a → (α a ≡ α x) ∨ (a ∋ x)) ψ X 199 Sup : {n : Level } → (ψ : ConstructibleSet → ConstructibleSet ) → (X : ConstructibleSet) → SupR (λ x a → (α a ≡ α x) ∨ (a ∋ x)) ψ X
179 sup (Sup ψ X ) = suptraverse X c∅ ψ 200 sup (Sup {n} ψ X ) = suptraverse X (c∅ {n}) ψ
180 smax (Sup ψ X ) = {!!} -- TransFinite {!!} {!!} {!!} {!!} {!!} 201 smax (Sup ψ X ) = {!!}
181 suniq (Sup ψ X ) = {!!} 202 suniq (Sup ψ X ) = {!!}
182 203
183
184 -- transitiveness : (a b c : ConstructibleSet ) → a ∋ b → b ∋ c → a ∋ c
185 -- transitiveness a b c a∋b b∋c with constructible a c∋ constructible b | constructible b c∋ constructible c
186 -- ... | t1 | t2 = {!!}
187
188 open import Data.Unit 204 open import Data.Unit
189 open SupR 205 open SupR
190 206
191 ConstructibleSet→ZF : ZF {suc (suc n)} {suc (suc n)} 207 ConstructibleSet→ZF : {n : Level} → ZF {suc n} {suc n}
192 ConstructibleSet→ZF = record { 208 ConstructibleSet→ZF {n} = record {
193 ZFSet = ConstructibleSet 209 ZFSet = ConstructibleSet
194 ; _∋_ = λ a b → Lift (suc (suc n)) ( a ∋ b ) 210 ; _∋_ = _∋_
195 ; _≈_ = _≡_ 211 ; _≈_ = _≡_
196 ; ∅ = c∅ 212 ; ∅ = c∅
197 ; _,_ = _,_ 213 ; _,_ = _,_
198 ; Union = Union 214 ; Union = Union
199 ; Power = {!!} 215 ; Power = {!!}
200 ; Select = Select 216 ; Select = Select
201 ; Replace = Replace 217 ; Replace = {!!}
202 ; infinite = {!!} 218 ; infinite = {!!}
203 ; isZF = {!!} 219 ; isZF = {!!}
204 } where 220 } where
205 conv : (ConstructibleSet → Set (suc (suc n))) → ConstructibleSet → Set (suc n) 221 conv : {n : Level} → (ConstructibleSet {n} → Set (suc (suc n))) → ConstructibleSet → Set (suc n)
206 conv ψ x with ψ x 222 conv {n} ψ x with ψ x
207 ... | t = Lift ( suc n ) ⊤ 223 ... | t = Lift ( suc n ) ⊤
208 Select : (X : ConstructibleSet) → (ConstructibleSet → Set (suc (suc n))) → ConstructibleSet 224 Select : (X : ConstructibleSet {n}) → (ConstructibleSet {n} → Set (suc n)) → ConstructibleSet {n}
209 Select X ψ = record { α = α X ; constructible = λ x → (conv ψ) (record { α = x ; constructible = λ x → constructible X x } ) } 225 Select X ψ = record { α = α X ; constructible = λ x → {!!} } -- ψ (record { α = x ; constructible = λ x → constructible X x } ) }
210 Replace : (X : ConstructibleSet) → (ConstructibleSet → ConstructibleSet) → ConstructibleSet 226 Replace : (X : ConstructibleSet {n} ) → (ConstructibleSet → ConstructibleSet) → ConstructibleSet
211 Replace X ψ = record { α = α (sup (Sup ψ X)) ; constructible = λ x → {!!} } 227 Replace X ψ = record { α = α (sup supψ) ; constructible = λ x → {!!} } where
212 _,_ : ConstructibleSet → ConstructibleSet → ConstructibleSet 228 supψ : SupR (λ x a → (α a ≡ α x) ∨ (a ∋ x)) ψ X
213 a , b = record { α = maxα (α a) (α b) ; constructible = λ x → {!!} } 229 supψ = Sup ψ X
230 repl : Ordinal {n} → Set (suc n)
231 repl x = {!!}
232 conv1 : (Ordinal {n} → Set n) → Ordinal {n} → Set n
233 conv1 ψ x with ψ
234 ... | t = Lift n ⊤
235 _,_ : ConstructibleSet {n} → ConstructibleSet → ConstructibleSet
236 a , b = record { α = maxα (α a) (α b) ; constructible = λ x → {!!} } -- ((x ≡ α a ) ∨ ( x ≡ α b )) }
214 Union : ConstructibleSet → ConstructibleSet 237 Union : ConstructibleSet → ConstructibleSet
215 Union a = {!!} 238 Union a = {!!}