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

annotate OPair.agda @ 324:fbabb20f222e

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 Sat, 04 Jul 2020 18:18:17 +0900
parents d9d3654baee1
children 5544f4921a44
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
277
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 272
diff changeset
20 open ODAxiom odAxiom
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 open _∧_
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 Bool
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25
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
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 <_,_> : (x y : OD) → OD
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 < x , y > = (x , x ) , (x , y )
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 exg-pair : { x y : OD } → (x , y ) == ( y , x )
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 exg-pair {x} {y} = record { eq→ = left ; eq← = right } where
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 left : {z : Ordinal} → def (x , y) z → def (y , x) z
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 left (case1 t) = case2 t
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 left (case2 t) = case1 t
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 right : {z : Ordinal} → def (y , x) z → def (x , y) z
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 right (case1 t) = case2 t
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 right (case2 t) = case1 t
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 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
42
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 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
44 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
45
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 eq-prod refl refl = refl
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 prod-eq : { x x' y y' : OD } → < x , y > == < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 prod-eq {x} {x'} {y} {y'} eq = record { proj1 = lemmax ; proj2 = lemmay } where
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 lemma0 : {x y z : OD } → ( x , x ) == ( z , y ) → x ≡ y
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 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
53 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
54 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
55 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
56 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
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<¬≡ s c )
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<¬≡ s c )
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 lemma2 : {x y z : OD } → ( x , x ) == ( z , y ) → z ≡ y
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 lemma2 {x} {y} {z} eq = trans (sym (lemma0 lemma3 )) ( lemma0 eq ) where
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 lemma3 : ( x , x ) == ( y , z )
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 lemma3 = ==-trans eq exg-pair
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 lemma1 : {x y : OD } → ( x , x ) == ( y , y ) → x ≡ y
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 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
66 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
67 lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s)
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 lemma4 : {x y z : OD } → ( x , y ) == ( x , z ) → y ≡ z
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 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
70 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
71 ... | refl with lemma2 (==-sym eq )
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 ... | refl = 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 | 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
74 lemmax : x ≡ x'
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 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
76 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
77 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
78 ... | refl = lemma1 (ord→== s )
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 lemmay : y ≡ y'
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 lemmay with lemmax
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 ... | 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
82 ... | 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
83
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 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
85 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
86
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 ZFProduct : OD
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 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
89
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 -- 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
91 -- 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
92 -- eq-pair refl refl = HE.refl
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 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
95 pi1 ( pair x y) = 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 π1 : { p : OD } → ZFProduct ∋ p → OD
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 π1 lt = ord→od (pi1 lt )
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 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
101 pi2 ( pair x y ) = y
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 π2 : { p : OD } → ZFProduct ∋ p → OD
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 π2 lt = ord→od (pi2 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 op-cons : { ox oy : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy >
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 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
108
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109 p-cons : ( x y : OD ) → ZFProduct ∋ < x , y >
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110 p-cons x y = def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl (
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 let open ≡-Reasoning in begin
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 od→ord < ord→od (od→ord x) , ord→od (od→ord y) >
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113 ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114 od→ord < x , y >
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115 ∎ )
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
117 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
118 op-iso (pair ox oy) = refl
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120 p-iso : { x : OD } → (p : ZFProduct ∋ x ) → < π1 p , π2 p > ≡ x
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121 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
122
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
123 p-pi1 : { x y : OD } → (p : ZFProduct ∋ < x , y > ) → π1 p ≡ x
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124 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
125
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 p-pi2 : { x y : OD } → (p : ZFProduct ∋ < x , y > ) → π2 p ≡ y
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127 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
128