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

comparison src/zorn.agda @ 488:d2d704ab1a33

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 Fri, 08 Apr 2022 17:36:42 +0900
parents 4fa7c5104b68
children dc7a95dd66c4
comparison
equal deleted inserted replaced
487:4fa7c5104b68 488:d2d704ab1a33
59 59
60 record SUP ( A B : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where 60 record SUP ( A B : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
61 field 61 field
62 sup : HOD 62 sup : HOD
63 A∋maximal : A ∋ sup 63 A∋maximal : A ∋ sup
64 x≤sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup ) -- B is Total 64 x≤sup : {x : HOD} → B ∋ x → (x ≡ sup ) ∨ (x < sup ) -- B is Total, use positive
65 65
66 record Maximal ( A : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where 66 record Maximal ( A : HOD ) (_<_ : (x y : HOD) → Set n ) : Set (suc n) where
67 field 67 field
68 maximal : HOD 68 maximal : HOD
69 A∋maximal : A ∋ maximal 69 A∋maximal : A ∋ maximal
105 record BX (x y : Ordinal) (fb : ( x : Ordinal ) → (x o< y ) → HOD ) : Set n where 105 record BX (x y : Ordinal) (fb : ( x : Ordinal ) → (x o< y ) → HOD ) : Set n where
106 field 106 field
107 bx : Ordinal 107 bx : Ordinal
108 bx<y : bx o< y 108 bx<y : bx o< y
109 is-fb : x ≡ & (fb bx bx<y ) 109 is-fb : x ≡ & (fb bx bx<y )
110 bx<A : (z : ZChain A (& A) _<_ ) → {x : Ordinal } → (bx : BX x (& A) ( ZChain.fb z )) → BX.bx bx o< & A
111 bx<A z {x} bx = BX.bx<y bx
110 B : (z : ZChain A (& A) _<_ ) → HOD 112 B : (z : ZChain A (& A) _<_ ) → HOD
111 B z = record { od = record { def = λ x → BX x (& A) ( ZChain.fb z ) } ; odmax = & A ; <odmax = {!!} } 113 B z = record { od = record { def = λ x → BX x (& A) ( ZChain.fb z ) } ; odmax = & A ; <odmax = {!!} }
112 z11 : (z : ZChain A (& A) _<_ ) → (x : Element (B z)) → elm x ≡ ZChain.fb z (BX.bx (is-elm x)) {!!} 114 z11 : (z : ZChain A (& A) _<_ ) → (x : Element (B z)) → elm x ≡ ZChain.fb z (BX.bx (is-elm x)) (bx<A z (is-elm x))
113 z11 z x = subst₂ (λ j k → j ≡ k ) *iso *iso ( cong (*) (BX.is-fb (is-elm x)) ) 115 z11 z x = subst₂ (λ j k → j ≡ k ) *iso *iso ( cong (*) (BX.is-fb (is-elm x)) )
114 obx : (z : ZChain A (& A) _<_ ) → {x : HOD} → B z ∋ x → Ordinal 116 obx : (z : ZChain A (& A) _<_ ) → {x : HOD} → B z ∋ x → Ordinal
115 obx z {x} bx = BX.bx bx 117 obx z {x} bx = BX.bx bx
116 obx=fb : (z : ZChain A (& A) _<_ ) → {x : HOD} → (bx : B z ∋ x ) → x ≡ ZChain.fb z ( obx z bx ) {!!} 118 obx=fb : (z : ZChain A (& A) _<_ ) → {x : HOD} → (bx : B z ∋ x ) → x ≡ ZChain.fb z ( obx z bx ) (bx<A z bx )
117 obx=fb z {x} bx = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) (BX.is-fb bx)) 119 obx=fb z {x} bx = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) (BX.is-fb bx))
120 B⊆A : (z : ZChain A (& A) _<_ ) → B z ⊆ A
121 B⊆A z = record { incl = λ {x} bx → subst (λ k → odef A k ) (sym (BX.is-fb bx)) (ZChain.A∋fb z (BX.bx bx) (BX.bx<y bx) ) }
122 PO-B : (z : ZChain A (& A) _<_ ) → PartialOrderSet (B z) _<_
123 PO-B z a b = PO record { elm = elm a ; is-elm = incl ( B⊆A z) (is-elm a) } record { elm = elm b ; is-elm = incl ( B⊆A z) (is-elm b) }
124 bx-monotonic : (z : ZChain A (& A) _<_ ) → {x y : Element (B z)} → obx z (is-elm x) o< obx z (is-elm y) → elm x < elm y
125 bx-monotonic z {x} {y} a = subst₂ (λ j k → j < k ) (sym (z11 z x)) (sym (z11 z y)) (ZChain.monotonic z (bx<A z (is-elm x)) (bx<A z (is-elm y)) a )
126 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
127 z12 : (z : ZChain A (& A) _<_ ) → {a b : HOD } → (x : BX (& a) (& A) (ZChain.fb z)) (y : BX (& b) (& A) (ZChain.fb z))
128 → obx z x ≡ obx z y → bx<A z x ≅ bx<A z y
129 z12 z {a} {b} x y eq = {!!}
130 bx-inject : (z : ZChain A (& A) _<_ ) → {x y : Element (B z)} → BX.bx (is-elm x) ≡ BX.bx (is-elm y) → elm x ≡ elm y
131 bx-inject z {x} {y} eq = begin
132 elm x ≡⟨ obx=fb z (is-elm x) ⟩
133 ZChain.fb z (obx z (is-elm x)) (bx<A z (is-elm x)) ≡⟨ cong₂ (λ j k → ZChain.fb z j k ) ? ( HE.≅-to-≡ (z12 z ? ? eq) ) ⟩
134 ZChain.fb z (obx z (is-elm y)) (bx<A z (is-elm y)) ≡⟨ sym ( obx=fb z (is-elm y) ) ⟩
135 elm y ∎ where open ≡-Reasoning
118 B-is-total : (z : ZChain A (& A) _<_ ) → TotalOrderSet (B z) _<_ 136 B-is-total : (z : ZChain A (& A) _<_ ) → TotalOrderSet (B z) _<_
119 B-is-total z x y with trio< (obx z (is-elm x)) (obx z (is-elm y)) 137 B-is-total z x y with trio< (obx z (is-elm x)) (obx z (is-elm y))
120 ... | tri< a ¬b ¬c = tri< z10 {!!} {!!} where 138 ... | tri< a ¬b ¬c = tri< z10 (λ eq → proj1 (proj2 (PO-B z x y) eq ) z10) (λ ¬c → proj1 (proj1 (PO-B z y x) ¬c ) z10) where
121 z10 : elm x < elm y 139 z10 : elm x < elm y
122 z10 = subst₂ (λ j k → j < k ) (sym (z11 z x)) (sym (z11 z y)) (ZChain.monotonic z {!!} {!!} a ) 140 z10 = bx-monotonic z {x} {y} a
123 ... | tri≈ ¬a b ¬c = tri≈ {!!} {!!} {!!} 141 ... | tri≈ ¬a b ¬c = tri≈ {!!} {!!} {!!}
124 ... | tri> ¬a ¬b c = tri> {!!} {!!} {!!} 142 ... | tri> ¬a ¬b c = tri> (λ ¬a → proj1 (proj1 (PO-B z x y) ¬a ) (bx-monotonic z {y} {x} c) ) (λ eq → proj2 (proj2 (PO-B z x y) eq ) (bx-monotonic z {y} {x} c)) (bx-monotonic z {y} {x} c)
125 B⊆A : (z : ZChain A (& A) _<_ ) → B z ⊆ A
126 B⊆A z = record { incl = λ {x} bx → subst (λ k → odef A k ) (sym (BX.is-fb bx)) (ZChain.A∋fb z (BX.bx bx) {!!} ) }
127 ZChain→¬SUP : (z : ZChain A (& A) _<_ ) → ¬ (SUP A (B z) _<_ ) 143 ZChain→¬SUP : (z : ZChain A (& A) _<_ ) → ¬ (SUP A (B z) _<_ )
128 ZChain→¬SUP z sp = ⊥-elim {!!} where 144 ZChain→¬SUP z sp = ⊥-elim {!!} where
129 z03 : & (SUP.sup sp) o< osuc (& A) 145 z03 : & (SUP.sup sp) o< osuc (& A)
130 z03 = ordtrans (c<→o< (SUP.A∋maximal sp)) <-osuc 146 z03 = ordtrans (c<→o< (SUP.A∋maximal sp)) <-osuc
131 z02 : (x : HOD) → B z ∋ x → SUP.sup sp < x → ⊥ 147 z02 : (x : HOD) → B z ∋ x → SUP.sup sp < x → ⊥