Mercurial > hg > Members > kono > Proof > ZF-in-agda
view ordinal-definable.agda @ 43:0d9b9db14361
equalitu and internal parametorisity
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 24 May 2019 22:22:16 +0900 |
parents | 4d5fc6381546 |
children | fcac01485f32 |
line wrap: on
line source
open import Level module ordinal-definable where open import zf open import ordinal open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) open import Relation.Binary.PropositionalEquality open import Data.Nat.Properties open import Data.Empty open import Relation.Nullary open import Relation.Binary open import Relation.Binary.Core -- Ordinal Definable Set record OD {n : Level} : Set (suc n) where field def : (x : Ordinal {n} ) → Set n open OD open import Data.Unit postulate od→ord : {n : Level} → OD {n} → Ordinal {n} ord→od : {n : Level} → Ordinal {n} → OD {n} _∋_ : { n : Level } → ( a x : OD {n} ) → Set n _∋_ {n} a x = def a ( od→ord x ) _c<_ : { n : Level } → ( a x : OD {n} ) → Set n x c< a = a ∋ x -- _=='_ : {n : Level} → Set (suc n) -- Rel (OD {n}) (suc n) -- _=='_ {n} = ( a b : OD {n} ) → ( ∀ { x : OD {n} } → a ∋ x → b ∋ x ) ∧ ( ∀ { x : OD {n} } → a ∋ x → b ∋ x ) record _==_ {n : Level} ( a b : OD {n} ) : Set n where field eq→ : ∀ { x : Ordinal {n} } → def a x → def b x eq← : ∀ { x : Ordinal {n} } → def b x → def a x id : {n : Level} {A : Set n} → A → A id x = x eq-refl : {n : Level} { x : OD {n} } → x == x eq-refl {n} {x} = record { eq→ = id ; eq← = id } open _==_ eq-sym : {n : Level} { x y : OD {n} } → x == y → y == x eq-sym eq = record { eq→ = eq← eq ; eq← = eq→ eq } eq-trans : {n : Level} { x y z : OD {n} } → x == y → y == z → x == z eq-trans x=y y=z = record { eq→ = λ t → eq→ y=z ( eq→ x=y t) ; eq← = λ t → eq← x=y ( eq← y=z t) } _c≤_ : {n : Level} → OD {n} → OD {n} → Set (suc n) a c≤ b = (a ≡ b) ∨ ( b ∋ a ) od∅ : {n : Level} → OD {n} od∅ {n} = record { def = λ _ → Lift n ⊥ } postulate c<→o< : {n : Level} {x y : OD {n} } → x c< y → od→ord x o< od→ord y o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → ord→od x c< ord→od y oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x sup-od : {n : Level } → ( OD {n} → OD {n}) → OD {n} sup-c< : {n : Level } → ( ψ : OD {n} → OD {n}) → ∀ {x : OD {n}} → ψ x c< sup-od ψ ∅-base-def : {n : Level} → def ( ord→od (o∅ {n}) ) ≡ def (od∅ {n}) ∅1 : {n : Level} → ( x : OD {n} ) → ¬ ( x c< od∅ {n} ) ∅1 {n} x (lift ()) ∅3 : {n : Level} → { x : Ordinal {n}} → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n} ∅3 {n} {x} = TransFinite {n} c1 c2 c3 x where c0 : Nat → Ordinal {n} → Set n c0 lx x = (∀(y : Ordinal {n}) → ¬ (y o< x)) → x ≡ o∅ {n} c1 : ∀ (lx : Nat ) → c0 lx (record { lv = Suc lx ; ord = ℵ lx } ) c1 lx not with not ( record { lv = lx ; ord = Φ lx } ) ... | t with t (case1 ≤-refl ) c1 lx not | t | () c2 : (lx : Nat) → c0 lx (record { lv = lx ; ord = Φ lx } ) c2 Zero not = refl c2 (Suc lx) not with not ( record { lv = lx ; ord = Φ lx } ) ... | t with t (case1 ≤-refl ) c2 (Suc lx) not | t | () c3 : (lx : Nat) (x₁ : OrdinalD lx) → c0 lx (record { lv = lx ; ord = x₁ }) → c0 lx (record { lv = lx ; ord = OSuc lx x₁ }) c3 lx (Φ .lx) d not with not ( record { lv = lx ; ord = Φ lx } ) ... | t with t (case2 Φ< ) c3 lx (Φ .lx) d not | t | () c3 lx (OSuc .lx x₁) d not with not ( record { lv = lx ; ord = OSuc lx x₁ } ) ... | t with t (case2 (s< s<refl ) ) c3 lx (OSuc .lx x₁) d not | t | () c3 (Suc lx) (ℵ lx) d not with not ( record { lv = Suc lx ; ord = OSuc (Suc lx) (Φ (Suc lx)) } ) ... | t with t (case2 (s< ℵΦ< )) c3 .(Suc lx) (ℵ lx) d not | t | () -- find : {n : Level} → ( x : Ordinal {n} ) → o∅ o< x → Ordinal {n} -- exists : {n : Level} → ( x : Ordinal {n} ) → (0<x : o∅ o< x ) → find x 0<x o< x def-subst : {n : Level } {Z : OD {n}} {X : Ordinal {n} }{z : OD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z → X ≡ x → def z x def-subst df refl refl = df transitive : {n : Level } { x y z : OD {n} } → y ∋ x → z ∋ y → z ∋ x transitive {n} {x} {y} {z} x∋y z∋y with ordtrans ( c<→o< {n} {x} {y} x∋y ) ( c<→o< {n} {y} {z} z∋y ) ... | t = lemma0 (lemma t) where lemma : ( od→ord x ) o< ( od→ord z ) → def ( ord→od ( od→ord z )) ( od→ord ( ord→od ( od→ord x ))) lemma xo<z = o<→c< xo<z lemma0 : def ( ord→od ( od→ord z )) ( od→ord ( ord→od ( od→ord x ))) → def z (od→ord x) lemma0 dz = def-subst {n} { ord→od ( od→ord z )} { od→ord ( ord→od ( od→ord x))} dz (oiso) (diso) record Minimumo {n : Level } (x : Ordinal {n}) : Set (suc n) where field mino : Ordinal {n} min<x : mino o< x ominimal : {n : Level} → (x : Ordinal {n} ) → o∅ o< x → Minimumo {n} x ominimal {n} record { lv = Zero ; ord = (Φ .0) } (case1 ()) ominimal {n} record { lv = Zero ; ord = (Φ .0) } (case2 ()) ominimal {n} record { lv = Zero ; ord = (OSuc .0 ord) } (case1 ()) ominimal {n} record { lv = Zero ; ord = (OSuc .0 ord) } (case2 Φ<) = record { mino = record { lv = Zero ; ord = Φ 0 } ; min<x = case2 Φ< } ominimal {n} record { lv = (Suc lv) ; ord = (Φ .(Suc lv)) } (case1 (s≤s x)) = record { mino = record { lv = lv ; ord = Φ lv } ; min<x = case1 (s≤s ≤-refl)} ominimal {n} record { lv = (Suc lv) ; ord = (Φ .(Suc lv)) } (case2 ()) ominimal {n} record { lv = (Suc lv) ; ord = (OSuc .(Suc lv) ord) } (case1 (s≤s x)) = record { mino = record { lv = (Suc lv) ; ord = ord } ; min<x = case2 s<refl} ominimal {n} record { lv = (Suc lv) ; ord = (OSuc .(Suc lv) ord) } (case2 ()) ominimal {n} record { lv = (Suc lv) ; ord = (ℵ .lv) } (case1 (s≤s z≤n)) = record { mino = record { lv = Suc lv ; ord = Φ (Suc lv) } ; min<x = case2 ℵΦ< } ominimal {n} record { lv = (Suc lv) ; ord = (ℵ .lv) } (case2 ()) ∅4 : {n : Level} → ( x : OD {n} ) → x ≡ od∅ {n} → od→ord x ≡ o∅ {n} ∅4 {n} x refl = ∅3 lemma1 where lemma0 : (y : Ordinal {n}) → def ( od∅ {n} ) y → ⊥ lemma0 y (lift ()) lemma1 : (y : Ordinal {n}) → y o< od→ord od∅ → ⊥ lemma1 y y<o = lemma0 y ( def-subst {n} {ord→od (od→ord od∅ )} {od→ord (ord→od y)} (o<→c< y<o) oiso diso ) ∅5 : {n : Level} → ( x : Ordinal {n} ) → ¬ ( x ≡ o∅ {n} ) → o∅ {n} o< x ∅5 {n} record { lv = Zero ; ord = (Φ .0) } not = ⊥-elim (not refl) ∅5 {n} record { lv = Zero ; ord = (OSuc .0 ord) } not = case2 Φ< ∅5 {n} record { lv = (Suc lv) ; ord = ord } not = case1 (s≤s z≤n) postulate extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n (suc n) ∅6 : {n : Level } ( x : Ordinal {suc n}) → o∅ o< x → ¬ x ≡ o∅ ∅6 {n} x lt eq with trio< {n} (o∅ {suc n}) x ∅6 {n} x lt refl | tri< a ¬b ¬c = ¬b refl ∅6 {n} x lt refl | tri≈ ¬a b ¬c = ¬a lt ∅6 {n} x lt refl | tri> ¬a ¬b c = ¬b refl ∅8 : {n : Level} → ( x : Ordinal {n} ) → ¬ x o< o∅ {n} ∅8 {n} x (case1 ()) ∅8 {n} x (case2 ()) -- ∅10 : {n : Level} → (x : OD {n} ) → ¬ ( ( y : OD {n} ) → Lift (suc n) ( x ∋ y)) → x ≡ od∅ -- ∅10 {n} x not = ? open Ordinal -- ∋-subst : {n : Level} {X Y x y : OD {suc n} } → X ≡ x → Y ≡ y → X ∋ Y → x ∋ y -- ∋-subst refl refl x = x -- ∅77 : {n : Level} → (x : OD {suc n} ) → ¬ ( ord→od (o∅ {suc n}) ∋ x ) -- ∅77 {n} x lt = {!!} where ∅7' : {n : Level} → ord→od (o∅ {n}) ≡ od∅ {n} ∅7' {n} = cong ( λ k → record { def = k }) ( ∅-base-def ) where ∅7 : {n : Level} → ( x : OD {n} ) → od→ord x ≡ o∅ {n} → x == od∅ {n} ∅7 {n} x eq = record { eq→ = e1 ; eq← = e2 } where e0 : {y : Ordinal {n}} → y o< o∅ {n} → def od∅ y e0 {y} (case1 ()) e0 {y} (case2 ()) e1 : {y : Ordinal {n}} → def x y → def od∅ y e1 {y} y<x = e0 ( o<-subst ( c<→o< {n} {x} y<x ) refl {!!} ) e2 : {y : Ordinal {n}} → def od∅ y → def x y e2 {y} (lift ()) ∅9 : {n : Level} → (x : OD {n} ) → ¬ x == od∅ → o∅ o< od→ord x ∅9 x not = ∅5 ( od→ord x) lemma where lemma : ¬ od→ord x ≡ o∅ lemma eq = not ( ∅7 x eq ) OD→ZF : {n : Level} → ZF {suc n} {n} OD→ZF {n} = record { ZFSet = OD {n} ; _∋_ = _∋_ ; _≈_ = _==_ ; ∅ = od∅ ; _,_ = _,_ ; Union = Union ; Power = Power ; Select = Select ; Replace = Replace ; infinite = record { def = λ x → x ≡ record { lv = Suc Zero ; ord = ℵ Zero } } ; isZF = isZF } where Replace : OD {n} → (OD {n} → OD {n} ) → OD {n} Replace X ψ = sup-od ψ Select : OD {n} → (OD {n} → Set n ) → OD {n} Select X ψ = record { def = λ x → select ( ord→od x ) } where select : OD {n} → Set n select x = ψ x _,_ : OD {n} → OD {n} → OD {n} x , y = record { def = λ z → ( (z ≡ od→ord x ) ∨ ( z ≡ od→ord y )) } Union : OD {n} → OD {n} Union x = record { def = λ y → {z : Ordinal {n}} → def x z → def (ord→od z) y } Power : OD {n} → OD {n} Power x = record { def = λ y → (z : Ordinal {n} ) → ( def x y ∧ def (ord→od z) y ) } ZFSet = OD {n} _∈_ : ( A B : ZFSet ) → Set n A ∈ B = B ∋ A _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set n _⊆_ A B {x} = A ∋ x → B ∋ x _∩_ : ( A B : ZFSet ) → ZFSet A ∩ B = Select (A , B) ( λ x → ( A ∋ x ) ∧ (B ∋ x) ) _∪_ : ( A B : ZFSet ) → ZFSet A ∪ B = Select (A , B) ( λ x → (A ∋ x) ∨ ( B ∋ x ) ) infixr 200 _∈_ infixr 230 _∩_ _∪_ infixr 220 _⊆_ isZF : IsZF (OD {n}) _∋_ _==_ od∅ _,_ Union Power Select Replace (record { def = λ x → x ≡ record { lv = Suc Zero ; ord = ℵ Zero } }) isZF = record { isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans } ; pair = pair ; union→ = {!!} ; union← = {!!} ; empty = empty ; power→ = {!!} ; power← = {!!} ; extentionality = {!!} ; minimul = minimul ; regularity = {!!} ; infinity∅ = {!!} ; infinity = {!!} ; selection = {!!} ; replacement = {!!} } where open _∧_ open Minimumo pair : (A B : OD {n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) proj1 (pair A B ) = case1 refl proj2 (pair A B ) = case2 refl empty : (x : OD {n} ) → ¬ (od∅ ∋ x) empty x () union→ : (X x y : OD {n} ) → (X ∋ x) → (x ∋ y) → (Union X ∋ y) union→ X x y X∋x x∋y = {!!} where lemma : {z : Ordinal {n} } → def X z → z ≡ od→ord y lemma {z} X∋z = {!!} minord : (x : OD {n} ) → ¬ (x == od∅ )→ Minimumo (od→ord x) minord x not = ominimal (od→ord x) (∅9 x not) minimul : (x : OD {n} ) → ¬ (x == od∅ )→ OD {n} minimul x not = ord→od ( mino (minord x not)) minimul<x : (x : OD {n} ) → (not : ¬ x == od∅ ) → x ∋ minimul x not minimul<x x not = lemma0 (min<x (minord x not)) where lemma0 : mino (minord x not) o< (od→ord x) → def x (od→ord (ord→od (mino (minord x not)))) lemma0 m<x = def-subst {n} {ord→od (od→ord x)} {od→ord (ord→od (mino (minord x not)))} (o<→c< m<x) oiso refl regularity : (x : OD) (not : ¬ (x == od∅)) → (x ∋ minimul x not) ∧ (Select (minimul x not , x) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) -- regularity : (x : OD) → (not : ¬ x == od∅ ) → -- ((x ∋ minimul x not ) ∧ {!!} ) -- (Select x (λ x₁ → (( minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅))) proj1 ( regularity x non ) = minimul<x x non proj2 ( regularity x non ) = {!!} where -- cong ( λ k → record { def = k } ) ( extensionality ( λ y → lemma0 y) ) where not-min : ( z : Ordinal {n} ) → ¬ ( def (Select x (λ y → (minimul x non ∋ y) ∧ (x ∋ y))) z ) not-min z = {!!} lemma0 : ( z : Ordinal {n} ) → def (Select x (λ y → (minimul x non ∋ y) ∧ (x ∋ y))) z ≡ Lift n ⊥ lemma0 z = {!!}