Members/kono/Proof/ZF-in-agda: OPair.agda annotate

annotate OPair.agda @ 361:4cbcf71b09c4

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Fri, 17 Jul 2020 16:33:30 +0900
parents	2a8a51375e49
children	8a430df110eb

rev	line source
272 985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	1 open import Level
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	2 open import Ordinals
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	3 module OPair {n : Level } (O : Ordinals {n}) where
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	4
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	5 open import zf
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	6 open import logic
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	7 import OD
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	8
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	9 open import Relation.Nullary
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	10 open import Relation.Binary
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	11 open import Data.Empty
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	12 open import Relation.Binary
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	13 open import Relation.Binary.Core
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	14 open import Relation.Binary.PropositionalEquality
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	15 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	16
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	17 open inOrdinal O
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	18 open OD O
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	19 open OD.OD
329 5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	20 open OD.HOD
277 d9d3654baee1 seperate choice from LEM Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 272 diff changeset	21 open ODAxiom odAxiom
272 985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	22
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	23 open _∧_
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	24 open _∨_
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	25 open Bool
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	26
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	27 open _==_
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	28
329 5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	29 _=h=_ : (x y : HOD) → Set n
5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	30 x =h= y = od x == od y
5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	31
5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	32 <_,_> : (x y : HOD) → HOD
272 985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	33 < x , y > = (x , x ) , (x , y )
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	34
329 5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	35 exg-pair : { x y : HOD } → (x , y ) =h= ( y , x )
272 985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	36 exg-pair {x} {y} = record { eq→ = left ; eq← = right } where
329 5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	37 left : {z : Ordinal} → odef (x , y) z → odef (y , x) z
272 985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	38 left (case1 t) = case2 t
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	39 left (case2 t) = case1 t
329 5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	40 right : {z : Ordinal} → odef (y , x) z → odef (x , y) z
272 985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	41 right (case1 t) = case2 t
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	42 right (case2 t) = case1 t
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	43
329 5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	44 ord≡→≡ : { x y : HOD } → od→ord x ≡ od→ord y → x ≡ y
272 985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	45 ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq )
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	46
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	47 od≡→≡ : { x y : Ordinal } → ord→od x ≡ ord→od y → x ≡ y
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	48 od≡→≡ eq = subst₂ (λ j k → j ≡ k ) diso diso ( cong ( λ k → od→ord k ) eq )
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	49
329 5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	50 eq-prod : { x x' y y' : HOD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
272 985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	51 eq-prod refl refl = refl
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	52
329 5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	53 prod-eq : { x x' y y' : HOD } → < x , y > =h= < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
272 985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	54 prod-eq {x} {x'} {y} {y'} eq = record { proj1 = lemmax ; proj2 = lemmay } where
329 5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	55 lemma0 : {x y z : HOD } → ( x , x ) =h= ( z , y ) → x ≡ y
272 985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	56 lemma0 {x} {y} eq with trio< (od→ord x) (od→ord y)
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	57 lemma0 {x} {y} eq \| tri< a ¬b ¬c with eq← eq {od→ord y} (case2 refl)
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	58 lemma0 {x} {y} eq \| tri< a ¬b ¬c \| case1 s = ⊥-elim ( o<¬≡ (sym s) a )
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	59 lemma0 {x} {y} eq \| tri< a ¬b ¬c \| case2 s = ⊥-elim ( o<¬≡ (sym s) a )
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	60 lemma0 {x} {y} eq \| tri≈ ¬a b ¬c = ord≡→≡ b
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	61 lemma0 {x} {y} eq \| tri> ¬a ¬b c with eq← eq {od→ord y} (case2 refl)
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	62 lemma0 {x} {y} eq \| tri> ¬a ¬b c \| case1 s = ⊥-elim ( o<¬≡ s c )
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	63 lemma0 {x} {y} eq \| tri> ¬a ¬b c \| case2 s = ⊥-elim ( o<¬≡ s c )
329 5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	64 lemma2 : {x y z : HOD } → ( x , x ) =h= ( z , y ) → z ≡ y
272 985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	65 lemma2 {x} {y} {z} eq = trans (sym (lemma0 lemma3 )) ( lemma0 eq ) where
329 5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	66 lemma3 : ( x , x ) =h= ( y , z )
272 985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	67 lemma3 = ==-trans eq exg-pair
329 5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	68 lemma1 : {x y : HOD } → ( x , x ) =h= ( y , y ) → x ≡ y
272 985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	69 lemma1 {x} {y} eq with eq← eq {od→ord y} (case2 refl)
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	70 lemma1 {x} {y} eq \| case1 s = ord≡→≡ (sym s)
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	71 lemma1 {x} {y} eq \| case2 s = ord≡→≡ (sym s)
329 5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	72 lemma4 : {x y z : HOD } → ( x , y ) =h= ( x , z ) → y ≡ z
272 985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	73 lemma4 {x} {y} {z} eq with eq← eq {od→ord z} (case2 refl)
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	74 lemma4 {x} {y} {z} eq \| case1 s with ord≡→≡ s -- x ≡ z
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	75 ... \| refl with lemma2 (==-sym eq )
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	76 ... \| refl = refl
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	77 lemma4 {x} {y} {z} eq \| case2 s = ord≡→≡ (sym s) -- y ≡ z
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	78 lemmax : x ≡ x'
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	79 lemmax with eq→ eq {od→ord (x , x)} (case1 refl)
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	80 lemmax \| case1 s = lemma1 (ord→== s ) -- (x,x)≡(x',x')
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	81 lemmax \| case2 s with lemma2 (ord→== s ) -- (x,x)≡(x',y') with x'≡y'
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	82 ... \| refl = lemma1 (ord→== s )
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	83 lemmay : y ≡ y'
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	84 lemmay with lemmax
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	85 ... \| refl with lemma4 eq -- with (x,y)≡(x,y')
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	86 ... \| eq1 = lemma4 (ord→== (cong (λ k → od→ord k ) eq1 ))
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	87
329 5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	88 --
5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	89 -- unlike ordered pair, ZFProduct is not a HOD
5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	90
272 985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	91 data ord-pair : (p : Ordinal) → Set n where
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	92 pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	93
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	94 ZFProduct : OD
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	95 ZFProduct = record { def = λ x → ord-pair x }
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	96
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	97 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	98 -- eq-pair : { x x' y y' : Ordinal } → x ≡ x' → y ≡ y' → pair x y ≅ pair x' y'
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	99 -- eq-pair refl refl = HE.refl
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	100
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	101 pi1 : { p : Ordinal } → ord-pair p → Ordinal
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	102 pi1 ( pair x y) = x
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	103
329 5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	104 π1 : { p : HOD } → def ZFProduct (od→ord p) → HOD
272 985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	105 π1 lt = ord→od (pi1 lt )
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	106
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	107 pi2 : { p : Ordinal } → ord-pair p → Ordinal
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	108 pi2 ( pair x y ) = y
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	109
329 5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	110 π2 : { p : HOD } → def ZFProduct (od→ord p) → HOD
272 985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	111 π2 lt = ord→od (pi2 lt )
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	112
329 5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	113 op-cons : { ox oy : Ordinal } → def ZFProduct (od→ord ( < ord→od ox , ord→od oy > ))
272 985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	114 op-cons {ox} {oy} = pair ox oy
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	115
329 5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	116 def-subst : {Z : OD } {X : Ordinal }{z : OD } {x : Ordinal }→ def Z X → Z ≡ z → X ≡ x → def z x
5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	117 def-subst df refl refl = df
5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	118
5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	119 p-cons : ( x y : HOD ) → def ZFProduct (od→ord ( < x , y >))
5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	120 p-cons x y = def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl (
5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	121 let open ≡-Reasoning in begin
5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	122 od→ord < ord→od (od→ord x) , ord→od (od→ord y) >
5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	123 ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩
5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	124 od→ord < x , y >
5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	125 ∎ )
272 985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	126
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	127 op-iso : { op : Ordinal } → (q : ord-pair op ) → od→ord < ord→od (pi1 q) , ord→od (pi2 q) > ≡ op
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	128 op-iso (pair ox oy) = refl
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	129
329 5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	130 p-iso : { x : HOD } → (p : def ZFProduct (od→ord x) ) → < π1 p , π2 p > ≡ x
272 985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	131 p-iso {x} p = ord≡→≡ (op-iso p)
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	132
329 5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	133 p-pi1 : { x y : HOD } → (p : def ZFProduct (od→ord < x , y >) ) → π1 p ≡ x
272 985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	134 p-pi1 {x} {y} p = proj1 ( prod-eq ( ord→== (op-iso p) ))
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	135
329 5544f4921a44 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 277 diff changeset	136 p-pi2 : { x y : HOD } → (p : def ZFProduct (od→ord < x , y >) ) → π2 p ≡ y
272 985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	137 p-pi2 {x} {y} p = proj2 ( prod-eq ( ord→== (op-iso p)))
985a1af11bce separate ordered pair and Boolean Algebra Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: diff changeset	138
360 2a8a51375e49 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 329 diff changeset	139
2a8a51375e49 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 329 diff changeset	140 _⊗_ : (A B : HOD) → HOD
2a8a51375e49 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 329 diff changeset	141 A ⊗ B = record { od = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } ;
2a8a51375e49 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 329 diff changeset	142 odmax = pmax; <odmax = <pmax } where
2a8a51375e49 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 329 diff changeset	143 checkAB : { p : Ordinal } → def ZFProduct p → Set n
2a8a51375e49 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 329 diff changeset	144 checkAB (pair x y) = odef A x ∧ odef B y
2a8a51375e49 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 329 diff changeset	145 pmax : Ordinal
361 4cbcf71b09c4 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 360 diff changeset	146 pmax = next (omax (od→ord A) (od→ord B))
4cbcf71b09c4 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 360 diff changeset	147 <pmax : {y : Ordinal} → def ZFProduct y ∧ ({x : Ordinal} (p : def ZFProduct x) → checkAB p) → y o< next (omax (od→ord A) (od→ord B))
4cbcf71b09c4 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 360 diff changeset	148 <pmax {y} prod = {!!} where
4cbcf71b09c4 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 360 diff changeset	149 prod-odmax : ( x y : HOD) → Ordinal
4cbcf71b09c4 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 360 diff changeset	150 prod-odmax x y = omax (od→ord (x , x)) (od→ord (x , y))
4cbcf71b09c4 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 360 diff changeset	151 lemma : {x y z : HOD } → ((x , x ) , (x , y )) ∋ z → od→ord z o< osuc (osuc (od→ord (x , y) ))
4cbcf71b09c4 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 360 diff changeset	152 lemma {x} {y} {z} = {!!}
4cbcf71b09c4 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 360 diff changeset	153 lemma1 : {x y : HOD } → A ∋ x → B ∋ y → od→ord (x , y) o< omax (odmax A) (odmax B)
4cbcf71b09c4 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 360 diff changeset	154 lemma1 {x} {y} A∋x B∋y with trio< (odmax A) (odmax B)
4cbcf71b09c4 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 360 diff changeset	155 lemma1 {x} {y} A∋x B∋y \| tri< a ¬b ¬c = begin
4cbcf71b09c4 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 360 diff changeset	156 od→ord (x , y)
4cbcf71b09c4 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 360 diff changeset	157 ≤⟨ {!!} ⟩
4cbcf71b09c4 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 360 diff changeset	158 odmax B
4cbcf71b09c4 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 360 diff changeset	159 ∎ where open o≤-Reasoning O
4cbcf71b09c4 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 360 diff changeset	160 lemma1 {x} {y} A∋x B∋y \| tri≈ ¬a b ¬c = {!!}
4cbcf71b09c4 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 360 diff changeset	161 lemma1 {x} {y} A∋x B∋y \| tri> ¬a ¬b c = {!!}
360 2a8a51375e49 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 329 diff changeset	162
361 4cbcf71b09c4 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 360 diff changeset	163 -- lemma2 : od→ord (x , y) o< osuc (omax (odmax A) (odmax B))
4cbcf71b09c4 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 360 diff changeset	164 -- lemma2 = begin
4cbcf71b09c4 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 360 diff changeset	165 -- {!!}
4cbcf71b09c4 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 360 diff changeset	166 -- ≤⟨ {!!} ⟩
4cbcf71b09c4 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 360 diff changeset	167 -- {!!}
4cbcf71b09c4 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 360 diff changeset	168 -- ∎ where open o≤-Reasoning O
4cbcf71b09c4 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 360 diff changeset	169 a = π1 (subst (λ k → def ZFProduct k) (sym diso) (proj1 prod))
4cbcf71b09c4 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 360 diff changeset	170 b = π2 (subst (λ k → def ZFProduct k) (sym diso) (proj1 prod))
4cbcf71b09c4 ... Shinji KONO <kono@ie.u-ryukyu.ac.jp> parents: 360 diff changeset	171

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

annotate OPair.agda @ 361:4cbcf71b09c4