Members/kono/Proof/ZF-in-agda: OD.agda comparison

comparison OD.agda @ 423:9984cdd88da3

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Sat, 01 Aug 2020 18:05:23 +0900
parents	44a484f17f26
children	cc7909f86841

comparison

equal deleted inserted replaced

-:44a484f17f26
+:9984cdd88da3
 record _==_  ( a b :  OD  ) : Set n where
 field
 eq→ : ∀ { x : Ordinal  } → def a x → def b x
 eq← : ∀ { x : Ordinal  } → def b x → def a x
-id : {A : Set n} → A → A
-id x = x
 ==-refl :  {  x :  OD  } → x == x
-==-refl  {x} = record { eq→ = id ; eq← = id }
+==-refl  {x} = record { eq→ = λ x → x ; eq← = λ x → x }
 open  _==_
 ==-trans : { x y z : OD } →  x == y →  y == z →  x ==  z
 ==-trans x=y y=z  = record { eq→ = λ {m} t → eq→ y=z (eq→ x=y t) ; eq← =  λ {m} t → eq← x=y (eq← y=z t) }
 x c< a = a ∋ x
 d→∋ : ( a : HOD  ) { x : Ordinal} → odef a x → a ∋ (* x)
 d→∋ a lt = subst (λ k → odef a k ) (sym &iso) lt
-cseq :  HOD  →  HOD
+-- odef-subst :  {Z : HOD } {X : Ordinal  }{z : HOD } {x : Ordinal  }→ odef Z X → Z ≡ z  →  X ≡ x  →  odef z x
-cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where
+-- odef-subst df refl refl = df
-lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x)
-lemma {y} lt = ordtrans <-osuc (ordtrans (<odmax x lt) <-osuc )
-odef-subst :  {Z : HOD } {X : Ordinal  }{z : HOD } {x : Ordinal  }→ odef Z X → Z ≡ z  →  X ≡ x  →  odef z x
-odef-subst df refl refl = df
 otrans : {a x y : Ordinal  } → odef (Ord a) x → odef (Ord x) y → odef (Ord a) y
 otrans x<a y<x = ordtrans y<x x<a
-odef→o< :  {X : HOD } → {x : Ordinal } → odef X x → x o< & X
-odef→o<  {X} {x} lt = o<-subst  {_} {_} {x} {& X} ( c<→o< ( odef-subst  {X} {x}  lt (sym *iso) (sym &iso) )) &iso &iso
-odefo→o< :  {X y : Ordinal } → odef (* X) y → y o< X
-odefo→o< {X} {y} lt = subst₂ (λ j k → j o< k ) &iso &iso ( c<→o< (subst (λ k → odef (* X) k ) (sym &iso ) lt ))
 -- If we have reverse of c<→o<, everything becomes Ordinal
 o<→c<→HOD=Ord : ( o<→c< : {x y : Ordinal  } → x o< y → odef (* y) x ) → {x : HOD } →  x ≡ Ord (& x)
 o<→c<→HOD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
 lemma1 : {y : Ordinal} → odef x y → odef (Ord (& x)) y
 orefl : { x : HOD  } → { y : Ordinal  } → & x ≡ y → & x ≡ y
 orefl refl = refl
 ==-iso : { x y : HOD  } → od (* (& x)) == od (* (& y))  →  od x == od y
 ==-iso  {x} {y} eq = record {
-eq→ = λ d →  lemma ( eq→  eq (odef-subst d (sym *iso) refl )) ;
+eq→ = λ {z} d →  lemma ( eq→  eq (subst (λ k → odef k z ) (sym *iso) d )) ;
-eq← = λ d →  lemma ( eq←  eq (odef-subst d (sym *iso) refl ))  }
+eq← = λ {z} d →  lemma ( eq←  eq (subst (λ k → odef k z ) (sym *iso) d )) }
 where
 lemma : {x : HOD  } {z : Ordinal } → odef (* (& x)) z → odef x z
-lemma {x} {z} d = odef-subst d *iso refl
+lemma {x} {z} d = subst (λ k → odef k z) (*iso) d
 =-iso :  {x y : HOD  } → (od x == od y) ≡ (od (* (& x)) == od y)
 =-iso  {_} {y} = cong ( λ k → od k == od y ) (sym *iso)
 ord→== : { x y : HOD  } → & x ≡  & y →  od x == od y
 o≡→==  {x} {.x} refl = ==-refl
 o∅≡od∅ : * (o∅ ) ≡ od∅
 o∅≡od∅  = ==→o≡ lemma where
 lemma0 :  {x : Ordinal} → odef (* o∅) x → odef od∅ x
-lemma0 {x} lt = o<-subst (c<→o<  {* x} {* o∅} (odef-subst  {* o∅} {x} lt refl (sym &iso)) ) &iso &iso
+lemma0 {x} lt with c<→o< {* x} {* o∅} (subst (λ k → odef (* o∅) k ) (sym &iso) lt)
+... | t = subst₂ (λ j k → j o< k ) &iso &iso t
 lemma1 :  {x : Ordinal} → odef od∅ x → odef (* o∅) x
 lemma1 {x} lt = ⊥-elim (¬x<0 lt)
 lemma : od (* o∅) == od od∅
 lemma = record { eq→ = lemma0 ; eq← = lemma1 }
 x , y = record { od = record { def = λ t → (t ≡ & x ) ∨ ( t ≡ & y ) } ; odmax = omax (& x)  (& y) ; <odmax = lemma }  where
 lemma : {t : Ordinal} → (t ≡ & x) ∨ (t ≡ & y) → t o< omax (& x) (& y)
 lemma {t} (case1 refl) = omax-x  _ _
 lemma {t} (case2 refl) = omax-y  _ _
-pair-xx<xy : {x y : HOD} → & (x , x) o< osuc (& (x , y) )
-pair-xx<xy {x} {y} = ⊆→o≤  lemma where
-lemma : {z : Ordinal} → def (od (x , x)) z → def (od (x , y)) z
-lemma {z} (case1 refl) = case1 refl
-lemma {z} (case2 refl) = case1 refl
-pair-<xy : {x y : HOD} → {n : Ordinal}  → & x o< next n →  & y o< next n  → & (x , y) o< next n
-pair-<xy {x} {y} {o} x<nn y<nn with trio< (& x) (& y) | inspect (omax (& x)) (& y)
-... | tri< a ¬b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx y<nn)) ho<
-... | tri> ¬a ¬b c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx x<nn)) ho<
-... | tri≈ ¬a b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (omax≡ _ _ b) (subst (λ k → osuc k o< next o) b (osuc<nx x<nn))) ho<
---  another form of infinite
--- pair-ord< :  {x : Ordinal } → Set n
-pair-ord< : {x : HOD } → ( {y : HOD } → & y o< next (odmax y) ) → & ( x , x ) o< next (& x)
-pair-ord< {x} ho< = subst (λ k → & (x , x) o< k ) lemmab0 lemmab1  where
-lemmab0 : next (odmax (x , x)) ≡ next (& x)
-lemmab0 = trans (cong (λ k → next k) (omxx _)) (sym nexto≡)
-lemmab1 : & (x , x) o< next ( odmax (x , x))
-lemmab1 = ho<
 pair<y : {x y : HOD } → y ∋ x  → & (x , x) o< osuc (& y)
 pair<y {x} {y} y∋x = ⊆→o≤ lemma where
 lemma : {z : Ordinal} → def (od (x , x)) z → def (od y) z
 lemma (case1 refl) = y∋x
 lemma (case2 refl) = y∋x
 field
 incl : { x : HOD } → A ∋ x →  B ∋ x
 open _⊆_
 infixr  220 _⊆_
-trans-⊆ :  { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C
-trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) }
-refl-⊆ : {A : HOD} → A ⊆ A
-refl-⊆ {A} = record { incl = λ x → x }
-od⊆→o≤  : {x y : HOD } → x ⊆ y → & x o< osuc (& y)
-od⊆→o≤ {x} {y} lt  =  ⊆→o≤ {x} {y} (λ {z} x>z  → subst (λ k → def (od y) k ) &iso (incl lt (d→∋ x x>z)))
 -- if we have & (x , x) ≡ osuc (& x),  ⊆→o≤ → c<→o<
 ⊆→o≤→c<→o< : ({x : HOD} → & (x , x) ≡ osuc (& x) )
 →  ({y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z) )
 →   {x y : HOD  }   → def (od y) ( & x ) → & x o< & y
 lemma (case2 refl) = refl
 y⊆x,x : {z : Ordinals.ord O} → def (od (x , x)) z → def (od y) z
 y⊆x,x {z} lt = subst (λ k → def (od y) k ) (lemma lt) y∋x
 lemma1 : osuc (& y) o< & (x , x)
 lemma1 = subst (λ k → osuc (& y) o< k ) (sym (peq {x})) (osucc c )
-subset-lemma : {A x : HOD  } → ( {y : HOD } →  x ∋ y → (A ∩ x ) ∋  y ) ⇔  ( x ⊆ A  )
-subset-lemma  {A} {x} = record {
-proj1 = λ lt  → record { incl = λ x∋z → proj1 (lt x∋z)  }
-; proj2 = λ x⊆A lt → ⟪ incl x⊆A lt , lt ⟫
-}
-power< : {A x : HOD  } → x ⊆ A → Ord (osuc (& A)) ∋ x
-power< {A} {x} x⊆A = ⊆→o≤  (λ {y} x∋y → subst (λ k →  def (od A) k) &iso (lemma y x∋y ) ) where
-lemma : (y : Ordinal) → def (od x) y → def (od A) (& (* y))
-lemma y x∋y = incl x⊆A (d→∋ x x∋y)
-open import Data.Unit
 ε-induction : { ψ : HOD  → Set n}
 → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
 → (x : HOD ) → ψ x
 ε-induction {ψ} ind x = subst (λ k → ψ k ) *iso (ε-induction-ord (osuc (& x)) <-osuc )  where
 --     ωmax : Ordinal
 --     <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax
 --
 -- infinite : HOD
 -- infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax }
-odsuc : (y : HOD) → HOD
-odsuc y = Union (y , (y , y))
 infinite : HOD
 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma }  where
 u : (y : Ordinal ) → HOD
 u y = Union (* y , (* y , * y))
 --- main recursion
 lemma : {y : Ordinal} → infinite-d y → y o< next o∅
 lemma {o∅} iφ = x<nx
 lemma (isuc {y} x) = next< (lemma x) (next< (subst (λ k → & (* y , (* y , * y)) o< next k) &iso lemma71 ) (nexto=n lemma1))
-ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next o∅
+empty : (x : HOD  ) → ¬  (od∅ ∋ x)
-ω<next-o∅ {y} lt = <odmax infinite lt
+empty x = ¬x<0
-nat→ω : Nat → HOD
-nat→ω Zero = od∅
-nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y))
-ω→nato : {y : Ordinal} → infinite-d y → Nat
-ω→nato iφ = Zero
-ω→nato (isuc lt) = Suc (ω→nato lt)
-ω→nat : (n : HOD) → infinite ∋ n → Nat
-ω→nat n = ω→nato
-ω∋nat→ω : {n : Nat} → def (od infinite) (& (nat→ω n))
-ω∋nat→ω {Zero} = subst (λ k → def (od infinite) k) (sym ord-od∅) iφ
-ω∋nat→ω {Suc n} = subst (λ k → def (od infinite) k) lemma (isuc ( ω∋nat→ω {n})) where
-lemma :  & (Union (* (& (nat→ω n)) , (* (& (nat→ω n)) , * (& (nat→ω n))))) ≡ & (nat→ω (Suc n))
-lemma = subst (λ k → & (Union (k , ( k , k ))) ≡ & (nat→ω (Suc n))) (sym *iso) refl
 _=h=_ : (x y : HOD) → Set n
 x =h= y  = od x == od y
-infixr  200 _∈_
--- infixr  230 _∩_ _∪_
 pair→ : ( x y t : HOD  ) →  (x , y)  ∋ t  → ( t =h= x ) ∨ ( t =h= y )
 pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j =h= k ) *iso *iso (o≡→== t≡x ))
 pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j =h= k ) *iso *iso (o≡→== t≡y ))
 pair← : ( x y t : HOD  ) → ( t =h= x ) ∨ ( t =h= y ) →  (x , y)  ∋ t
 pair← x y t (case1 t=h=x) = case1 (cong (λ k → & k ) (==→o≡ t=h=x))
 pair← x y t (case2 t=h=y) = case2 (cong (λ k → & k ) (==→o≡ t=h=y))
-pair1 : { x y  : HOD  } →  (x , y ) ∋ x
-pair1 = case1 refl
-pair2 : { x y  : HOD  } →  (x , y ) ∋ y
-pair2 = case2 refl
-single : {x y : HOD } → (x , x ) ∋ y → x ≡ y
-single (case1 eq) = ==→o≡ ( ord→== (sym eq) )
-single (case2 eq) = ==→o≡ ( ord→== (sym eq) )
-empty : (x : HOD  ) → ¬  (od∅ ∋ x)
-empty x = ¬x<0
 o<→c< :  {x y : Ordinal } → x o< y → (Ord x) ⊆ (Ord y)
 o<→c< lt = record { incl = λ z → ordtrans z lt }
 ⊆→o< :  {x y : Ordinal } → (Ord x) ⊆ (Ord y) →  x o< osuc y
 ⊆→o< {x} {y}  lt with trio< x y
 ⊆→o< {x} {y}  lt | tri< a ¬b ¬c = ordtrans a <-osuc
 ⊆→o< {x} {y}  lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc
 ⊆→o< {x} {y}  lt | tri> ¬a ¬b c with (incl lt)  (o<-subst c (sym &iso) refl )
 ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt &iso refl ))
-open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
--- postulate f-extensionality : { n m : Level}  → HE.Extensionality n m
-ω-prev-eq1 : {x y : Ordinal} →  & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → ¬ (x o< y)
-ω-prev-eq1 {x} {y} eq x<y = eq→ (ord→== eq) {& (* y)} (λ not2 → not2 (& (* y , * y))
-⟪ case2 refl , subst (λ k → odef k (& (* y))) (sym *iso) (case1 refl)⟫ ) (λ u → lemma u ) where
-lemma : (u : Ordinal) → ¬ def (od (* x , (* x , * x))) u ∧ def (od (* u)) (& (* y))
-lemma u t with proj1 t
-lemma u t | case1 u=x = o<> (c<→o< {* y} {* u} (proj2 t)) (subst₂ (λ j k → j o< k )
-(trans (sym &iso) (trans (sym u=x) (sym &iso)) ) (sym &iso) x<y ) -- x ≡ & (* u)
-lemma u t | case2 u=xx = o<¬≡ (lemma1 (subst (λ k → odef k (& (* y)) ) (trans (cong (λ k → * k ) u=xx) *iso )  (proj2 t))) x<y where
-lemma1 : {x y : Ordinal } → (* x , * x ) ∋ * y → x ≡ y    --  y = x ∈ ( x , x ) = u
-lemma1 (case1 eq) = subst₂ (λ j k → j ≡ k ) &iso &iso (sym eq)
-lemma1 (case2 eq) = subst₂ (λ j k → j ≡ k ) &iso &iso (sym eq)
-ω-prev-eq : {x y : Ordinal} →  & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → x ≡ y
-ω-prev-eq {x} {y} eq with trio< x y
-ω-prev-eq {x} {y} eq | tri< a ¬b ¬c = ⊥-elim (ω-prev-eq1 eq a)
-ω-prev-eq {x} {y} eq | tri≈ ¬a b ¬c = b
-ω-prev-eq {x} {y} eq | tri> ¬a ¬b c = ⊥-elim (ω-prev-eq1 (sym eq) c)
-ω-∈s : (x : HOD) →  Union ( x , (x , x)) ∋ x
-ω-∈s x not = not (& (x , x)) ⟪ case2 refl , subst (λ k → odef k (& x) ) (sym *iso) (case1 refl) ⟫
-ωs≠0 : (x : HOD) →  ¬ ( Union ( x , (x , x)) ≡ od∅ )
-ωs≠0 y eq =  ⊥-elim ( ¬x<0 (subst (λ k → & y  o< k ) ord-od∅ (c<→o< (subst (λ k → odef k (& y )) eq (ω-∈s y) ))) )
-nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i
-nat→ω-iso {i} = ε-induction1 {λ i →  (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i  } ind i where
-ind : {x : HOD} → ({y : HOD} → x ∋ y → (lt : infinite ∋ y) → nat→ω (ω→nat y lt) ≡ y) →
-(lt : infinite ∋ x) → nat→ω (ω→nat x lt) ≡ x
-ind {x} prev lt = ind1 lt *iso where
-ind1 : {ox : Ordinal } → (ltd : infinite-d ox ) → * ox ≡ x → nat→ω (ω→nato ltd) ≡ x
-ind1 {o∅} iφ refl = sym o∅≡od∅
-ind1 (isuc {x₁} ltd) ox=x = begin
-nat→ω (ω→nato (isuc ltd) )
-≡⟨⟩
-Union (nat→ω (ω→nato ltd) , (nat→ω (ω→nato ltd) , nat→ω (ω→nato ltd)))
-≡⟨ cong (λ k → Union (k , (k , k ))) lemma  ⟩
-Union (* x₁ , (* x₁ , * x₁))
-≡⟨ trans ( sym *iso) ox=x ⟩
-x
-∎ where
-open ≡-Reasoning
-lemma0 :  x ∋ * x₁
-lemma0 = subst (λ k → odef k (& (* x₁))) (trans (sym *iso) ox=x) (λ not → not
-(& (* x₁ , * x₁))  ⟪ pair2 , subst (λ k → odef k (& (* x₁))) (sym *iso) pair1 ⟫ )
-lemma1 : infinite ∋ * x₁
-lemma1 = subst (λ k → odef infinite k) (sym &iso) ltd
-lemma3 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ltd ≅ ltd1
-lemma3 iφ iφ refl = HE.refl
-lemma3 iφ (isuc {y} ltd1) eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso eq (c<→o< (ω-∈s (* y)) )))
-lemma3 (isuc {y} ltd)  iφ eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso (sym eq) (c<→o< (ω-∈s (* y)) )))
-lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (ω-prev-eq (sym eq))
-... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅  (ω-prev-eq eq)) t
-lemma2 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ω→nato ltd ≡ ω→nato ltd1
-lemma2 {x} {y} ltd ltd1 eq = lemma6 eq (lemma3 {x} {y} ltd ltd1 eq)  where
-lemma6 : {x y : Ordinal} → {ltd : infinite-d x } {ltd1 : infinite-d y } → y ≡ x → ltd ≅ ltd1 → ω→nato ltd ≡ ω→nato ltd1
-lemma6 refl HE.refl = refl
-lemma :  nat→ω (ω→nato ltd) ≡ * x₁
-lemma = trans  (cong (λ k →  nat→ω  k) (lemma2 {x₁} {_} ltd (subst (λ k → infinite-d k ) (sym &iso) ltd)  &iso ) ) ( prev {* x₁} lemma0 lemma1 )
-ω→nat-iso : {i : Nat} → ω→nat ( nat→ω i ) (ω∋nat→ω {i}) ≡ i
-ω→nat-iso {i} = lemma i (ω∋nat→ω {i}) *iso where
-lemma : {x : Ordinal } → ( i : Nat ) → (ltd : infinite-d x ) → * x ≡  nat→ω i → ω→nato ltd ≡ i
-lemma {x} Zero iφ eq = refl
-lemma {x} (Suc i) iφ eq = ⊥-elim ( ωs≠0 (nat→ω i) (trans (sym eq) o∅≡od∅ )) -- Union (nat→ω i , (nat→ω i , nat→ω i)) ≡ od∅
-lemma Zero (isuc {x} ltd) eq = ⊥-elim ( ωs≠0 (* x) (subst (λ k → k ≡ od∅  ) *iso eq ))
-lemma (Suc i) (isuc {x} ltd) eq = cong (λ k → Suc k ) (lemma i ltd (lemma1 eq) )  where -- * x ≡ nat→ω i
-lemma1 :  * (& (Union (* x , (* x , * x)))) ≡ Union (nat→ω i , (nat→ω i , nat→ω i)) → * x ≡ nat→ω i
-lemma1 eq = subst (λ k → * x ≡ k ) *iso (cong (λ k → * k)
-( ω-prev-eq (subst (λ k → _ ≡ k ) &iso (cong (λ k → & k ) (sym
-(subst (λ k → _ ≡ Union ( k , ( k , k ))) (sym *iso ) eq ))))))
 ψiso :  {ψ : HOD  → Set n} {x y : HOD } → ψ x → x ≡ y   → ψ y
 ψiso {ψ} t refl = t
 selection : {ψ : HOD → Set n} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
 selection {ψ} {X} {y} = ⟪
 sup-c< :  (ψ : HOD → HOD) → {X x : HOD} → X ∋ x  → & (ψ x) o< (sup-o X (λ y X∋y → & (ψ (* y))))
 sup-c< ψ {X} {x} lt = subst (λ k → & (ψ k) o< _ ) *iso (sup-o< X lt )
 replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace X ψ ∋ ψ x
 replacement← {ψ} X x lt = ⟪ sup-c< ψ {X} {x} lt , lemma ⟫ where
 lemma : def (in-codomain X ψ) (& (ψ x))
-lemma not = ⊥-elim ( not ( & x ) (⟪ lt , cong (λ k → & (ψ k)) (sym *iso)⟫ ))
+lemma not = ⊥-elim ( not ( & x ) ⟪ lt , cong (λ k → & (ψ k)) (sym *iso)⟫ )
 replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y))
 replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
 lemma2 :  ¬ ((y : Ordinal) → ¬ odef X y ∧ ((& x) ≡ & (ψ (* y))))
 → ¬ ((y : Ordinal) → ¬ odef X y ∧ (* (& x) =h= ψ (* y)))
-lemma2 not not2  = not ( λ y d →  not2 y (⟪ proj1 d , lemma3 (proj2 d)⟫)) where
+lemma2 not not2  = not ( λ y d →  not2 y ⟪ proj1 d , lemma3 (proj2 d)⟫) where
 lemma3 : {y : Ordinal } → (& x ≡ & (ψ (*  y))) → (* (& x) =h= ψ (* y))
 lemma3 {y} eq = subst (λ k  → * (& x) =h= k ) *iso (o≡→== eq )
 lemma :  ( (y : HOD) → ¬ (x =h= ψ y)) → ( (y : Ordinal) → ¬ odef X y ∧ (* (& x) =h= ψ (* y)) )
 lemma not y not2 = not (* y) (subst (λ k → k =h= ψ (* y)) *iso  ( proj2 not2 ))
 --- A ∩ x =  record { def = λ y → odef A y ∧  odef x y }                   subset of A
 --
 --
 ∩-≡ :  { a b : HOD  } → ({x : HOD  } → (a ∋ x → b ∋ x)) → a =h= ( b ∩ a )
 ∩-≡ {a} {b} inc = record {
-eq→ = λ {x} x<a → ⟪ odef-subst  {_} {_} {b} {x} (inc (d→∋ a x<a)) refl &iso , x<a  ⟫ ;
+eq→ = λ {x} x<a → ⟪ (subst (λ k → odef b k ) &iso (inc (d→∋ a x<a))) , x<a  ⟫ ;
 eq← = λ {x} x<a∩b → proj2 x<a∩b }
 --
 -- Transitive Set case
 -- we have t ∋ x → Ord a ∋ x means t is a subset of Ord a, that is (Ord a) ∩ t =h= t
 -- OPwr (Ord a) is a sup of (Ord a) ∩ t, so OPwr (Ord a) ∋ t
 -- OPwr  A = Ord ( sup-o ( λ x → & ( A ∩ (* x )) ) )
 --
 ord-power← : (a : Ordinal ) (t : HOD) → ({x : HOD} → (t ∋ x → (Ord a) ∋ x)) → OPwr (Ord a) ∋ t
-ord-power← a t t→A  = odef-subst  {_} {_} {OPwr (Ord a)} {& t}
+ord-power← a t t→A  = subst (λ k → odef (OPwr (Ord a)) k ) (lemma1 lemma-eq) lemma where
-lemma refl (lemma1 lemma-eq )where
 lemma-eq :  ((Ord a) ∩ t) =h= t
 eq→ lemma-eq {z} w = proj2 w
-eq← lemma-eq {z} w = ⟪ odef-subst  {_} {_} {(Ord a)} {z} ( t→A (d→∋ t w)) refl &iso  , w ⟫
+eq← lemma-eq {z} w = ⟪ subst (λ k → odef (Ord a) k ) &iso ( t→A (d→∋ t w)) , w ⟫
 lemma1 :  {a : Ordinal } { t : HOD }
 → (eq : ((Ord a) ∩ t) =h= t)  → & ((Ord a) ∩ (* (& t))) ≡ & t
 lemma1  {a} {t} eq = subst (λ k → & ((Ord a) ∩ k) ≡ & t ) (sym *iso) (cong (λ k → & k ) (==→o≡ eq ))
 lemma2 : (& t) o< (osuc (& (Ord a)))
 lemma2 = ⊆→o≤  {t} {Ord a} (λ {x} x<t → subst (λ k → def (od (Ord a)) k) &iso (t→A (d→∋ t x<t)))
 lemmaj = subst₂ (λ j k → j o< k ) &iso lemmak lt
 lemma1 : & t o< sup-o (OPwr (Ord (& A))) (λ x lt → & (A ∩ (* x)))
 lemma1 = subst (λ k → & k o< sup-o (OPwr (Ord (& A)))  (λ x lt → & (A ∩ (* x))))
 lemma4 (sup-o< (OPwr (Ord (& A))) lemma7 )
 lemma2 :  def (in-codomain (OPwr (Ord (& A))) (_∩_ A)) (& t)
-lemma2 not = ⊥-elim ( not (& t) (⟪ lemma3 , lemma6 ⟫) ) where
+lemma2 not = ⊥-elim ( not (& t) ⟪ lemma3 , lemma6 ⟫ ) where
 lemma6 : & t ≡ & (A ∩ * (& t))
 lemma6 = cong ( λ k → & k ) (==→o≡ (subst (λ k → t =h= (A ∩ k)) (sym *iso) ( ∩-≡ {t} {A} t→A  )))
-ord⊆power : (a : Ordinal) → (Ord (osuc a)) ⊆ (Power (Ord a))
-ord⊆power a = record { incl = λ {x} lt →  power← (Ord a) x (lemma lt) } where
-lemma : {x y : HOD} → & x o< osuc a → x ∋ y →  Ord a ∋ y
-lemma lt y<x with osuc-≡< lt
-lemma lt y<x | case1 refl = c<→o< y<x
-lemma lt y<x | case2 x<a = ordtrans (c<→o< y<x) x<a
-continuum-hyphotheis : (a : Ordinal) → Set (suc n)
-continuum-hyphotheis a = Power (Ord a) ⊆ Ord (osuc a)
 extensionality0 : {A B : HOD } → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → A =h= B
 eq→ (extensionality0 {A} {B} eq ) {x} d = odef-iso  {A} {B} (sym &iso) (proj1 (eq (* x))) d
 eq← (extensionality0 {A} {B} eq ) {x} d = odef-iso  {B} {A} (sym &iso) (proj2 (eq (* x))) d
 extensionality : {A B w : HOD  } → ((z : HOD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B)
 proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d
 proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d
 infinity∅ : infinite  ∋ od∅
-infinity∅ = odef-subst  {_} {_} {infinite} {& (od∅ )} iφ refl lemma where
+infinity∅ = subst (λ k → odef infinite k ) lemma iφ where
 lemma : o∅ ≡ & od∅
 lemma =  let open ≡-Reasoning in begin
 o∅
 ≡⟨ sym &iso ⟩
 & ( * o∅ )
 ≡⟨ cong ( λ k → & k ) o∅≡od∅ ⟩
 & od∅
 ∎
 infinity : (x : HOD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
-infinity x lt = odef-subst  {_} {_} {infinite} {& (Union (x , (x , x )))} ( isuc {& x} lt ) refl lemma where
+infinity x lt = subst (λ k → odef infinite k ) lemma (isuc {& x} lt) where
 lemma :  & (Union (* (& x) , (* (& x) , * (& x))))
 ≡ & (Union (x , (x , x)))
 lemma = cong (λ k → & (Union ( k , ( k , k ) ))) *iso
 isZF : IsZF (HOD )  _∋_  _=h=_ od∅ _,_ Union Power Select Replace infinite
 ;   infinity∅ = infinity∅
 ;   infinity = infinity
 ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
 ;   replacement← = replacement←
 ;   replacement→ = λ {ψ} → replacement→ {ψ}
--- ;   choice-func = choice-func
--- ;   choice = choice
 }
 HOD→ZF : ZF
 HOD→ZF   = record {
 ZFSet = HOD

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

comparison OD.agda @ 423:9984cdd88da3