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

annotate OPair.agda @ 403:ce2ce3f62023

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 Tue, 28 Jul 2020 10:51:08 +0900
parents 6c72bee25653
children 6dcea4c7cba1
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
363
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 362
diff changeset
1 {-# OPTIONS --allow-unsolved-metas #-}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 362
diff changeset
2
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Level
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Ordinals
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 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
6
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import zf
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import logic
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 import OD
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import Relation.Nullary
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 Data.Empty
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 open import Relation.Binary
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 open import Relation.Binary.Core
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 open import Relation.Binary.PropositionalEquality
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 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
18
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 open inOrdinal O
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 open OD O
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 open OD.OD
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
22 open OD.HOD
277
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 272
diff changeset
23 open ODAxiom odAxiom
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 open _∧_
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 open _∨_
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 open Bool
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 open _==_
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
31 <_,_> : (x y : HOD) → HOD
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 < x , y > = (x , x ) , (x , y )
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
34 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
35 exg-pair {x} {y} = record { eq→ = left ; eq← = right } where
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
36 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
37 left (case1 t) = case2 t
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 left (case2 t) = case1 t
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
39 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
40 right (case1 t) = case2 t
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 right (case2 t) = case1 t
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
43 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
44 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
45
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 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
47 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
48
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
49 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
50 eq-prod refl refl = refl
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
52 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
53 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
54 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
55 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
56 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
57 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
58 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
59 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
60 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
61 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
62 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
63 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
64 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
65 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
66 lemma3 = ==-trans eq exg-pair
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
67 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
68 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
69 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
70 lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s)
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
71 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
72 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
73 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
74 ... | refl with lemma2 (==-sym eq )
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 ... | refl = refl
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 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
77 lemmax : x ≡ x'
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 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
79 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
80 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
81 ... | refl = lemma1 (ord→== s )
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 lemmay : y ≡ y'
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 lemmay with lemmax
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 ... | 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
85 ... | 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
86
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
87 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
88 -- unlike ordered pair, ZFProduct is not a HOD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
89
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 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
91 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
92
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 ZFProduct : OD
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 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
95
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 -- 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
97 -- 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
98 -- eq-pair refl refl = HE.refl
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 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
101 pi1 ( pair x y) = x
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
103 π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
104 π1 lt = ord→od (pi1 lt )
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 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
107 pi2 ( pair x y ) = y
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
109 π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
110 π2 lt = ord→od (pi2 lt )
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
112 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
113 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
114
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
115 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
116 def-subst df refl refl = df
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
117
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
118 p-cons : ( x y : HOD ) → def ZFProduct (od→ord ( < x , y >))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
119 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
120 let open ≡-Reasoning in begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
121 od→ord < ord→od (od→ord x) , ord→od (od→ord y) >
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
122 ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
123 od→ord < x , y >
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
124 ∎ )
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 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
127 op-iso (pair ox oy) = refl
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
129 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
130 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
131
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
132 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
133 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
134
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
135 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
136 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
137
368
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
138 ω-pair : {x y : HOD} → infinite ∋ x → infinite ∋ y → od→ord < x , y > o< next o∅
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
139 ω-pair {x} {y} lx ly = lemma where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
140 lemma1 : od→ord x o< od→ord y → od→ord ( x , x ) o< od→ord ( x , y )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
141 lemma1 = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
142 lemma0 : od→ord x o< od→ord y → od→ord < x , y > o< osuc (next (od→ord (x , y)))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
143 lemma0 x<y = begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
144 od→ord < x , y >
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
145 <⟨ ho< ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
146 next (omax (od→ord (x , x)) (od→ord (x , y)))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
147 ≡⟨ cong (λ k → next k ) (sym (omax< _ _ (lemma1 x<y))) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
148 next (osuc (od→ord (x , y)))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
149 ≡⟨ sym (nexto≡) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
150 next (od→ord (x , y))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
151 ∎ where open o≤-Reasoning O
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
152 lemma : od→ord < x , y > o< next o∅
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
153 lemma with trio< (od→ord x) (od→ord y)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
154 lemma | tri< a ¬b ¬c = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
155 lemma | tri≈ ¬a b ¬c = next< {!!} {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
156 lemma | tri> ¬a ¬b c = {!!}
367
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
157
362
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 361
diff changeset
158 _⊗_ : (A B : HOD) → HOD
376
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 369
diff changeset
159 A ⊗ B = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))
360
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
160
362
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 361
diff changeset
161 product→ : {A B a b : HOD} → A ∋ a → B ∋ b → ( A ⊗ B ) ∋ < a , b >
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 361
diff changeset
162 product→ {A} {B} {a} {b} A∋a B∋b = {!!}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 361
diff changeset
163
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 361
diff changeset
164 record IsProduct (A B p : HOD) (A⊗B∋p : (A ⊗ B ) ∋ p ) : Set (suc n) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 361
diff changeset
165 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 361
diff changeset
166 is-pair : def ZFProduct (od→ord p)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 361
diff changeset
167 π1A : A ∋ π1 is-pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 361
diff changeset
168 π2B : B ∋ π2 is-pair
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 361
diff changeset
169
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 361
diff changeset
170 product← : {A B a b p : HOD} → (lt : (A ⊗ B ) ∋ p ) → IsProduct A B p lt
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 361
diff changeset
171 product← lt = record { is-pair = {!!} ; π1A = {!!} ; π2B = {!!} }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 361
diff changeset
172
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 361
diff changeset
173
367
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
174 ZFP : (A B : HOD) → HOD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
175 ZFP A B = record { od = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } ;
362
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 361
diff changeset
176 odmax = {!!} ; <odmax = {!!} } where
360
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
177 checkAB : { p : Ordinal } → def ZFProduct p → Set n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
178 checkAB (pair x y) = odef A x ∧ odef B y