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

annotate OPair.agda @ 360:2a8a51375e49

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 Wed, 15 Jul 2020 08:42:30 +0900
parents 5544f4921a44
children 4cbcf71b09c4
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
29 _=h=_ : (x y : HOD) → Set n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
30 x =h= y = od x == od y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
31
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
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
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
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
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
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
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
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
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
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
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
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
88 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
89 -- unlike ordered pair, ZFProduct is not a HOD
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
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
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
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
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
117 def-subst df refl refl = df
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
118
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
119 p-cons : ( x y : HOD ) → def ZFProduct (od→ord ( < x , y >))
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 (
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
121 let open ≡-Reasoning in begin
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) >
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
123 ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
124 od→ord < x , y >
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
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
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
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
139
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
140 _⊗_ : (A B : HOD) → HOD
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 ) } ;
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
142 odmax = pmax; <odmax = <pmax } where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
143 checkAB : { p : Ordinal } → def ZFProduct p → Set n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
144 checkAB (pair x y) = odef A x ∧ odef B y
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
145 pmax : Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
146 pmax = omax (odmax A) (odmax B)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
147 <pmax : {y : Ordinal} → def ZFProduct y ∧ ({x : Ordinal} (p : def ZFProduct x) → checkAB p) → y o< omax (odmax A) (odmax B)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
148 <pmax {y} = TransFinite {λ y → def ZFProduct y ∧ ({x : Ordinal} (p : def ZFProduct x) → checkAB p) → y o< omax (odmax A) (odmax B)} ind y where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
149 ind : (x : Ordinal)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
150 → ((y₁ : Ordinal) → y₁ o< x → def ZFProduct y₁ ∧ ({x₁ : Ordinal} (p : def ZFProduct x₁) → checkAB p) → y₁ o< (omax (odmax A) (odmax B)))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
151 → def ZFProduct x ∧ ({x₁ : Ordinal} (p : def ZFProduct x₁) → checkAB p) → x o< (omax (HOD.odmax A) (HOD.odmax B))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
152 ind = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
153