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

annotate OPair.agda @ 424:cc7909f86841

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remvoe TransFinifte1
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 01 Aug 2020 23:37:10 +0900
parents 44a484f17f26
children f7d66c84bc26
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
424
cc7909f86841 remvoe TransFinifte1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 422
diff changeset
10 import ODUtil
cc7909f86841 remvoe TransFinifte1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 422
diff changeset
11 import OrdUtil
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 open import Relation.Nullary
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 Data.Empty
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 open import Relation.Binary
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 open import Relation.Binary.Core
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 open import Relation.Binary.PropositionalEquality
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 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
20
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 open inOrdinal O
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 open OD O
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 open OD.OD
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
24 open OD.HOD
277
d9d3654baee1 seperate choice from LEM
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 272
diff changeset
25 open ODAxiom odAxiom
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26
424
cc7909f86841 remvoe TransFinifte1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 422
diff changeset
27 open Ordinals.Ordinals O
cc7909f86841 remvoe TransFinifte1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 422
diff changeset
28 open Ordinals.IsOrdinals isOrdinal
cc7909f86841 remvoe TransFinifte1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 422
diff changeset
29 open Ordinals.IsNext isNext
cc7909f86841 remvoe TransFinifte1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 422
diff changeset
30 open OrdUtil O
cc7909f86841 remvoe TransFinifte1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 422
diff changeset
31 open ODUtil O
cc7909f86841 remvoe TransFinifte1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 422
diff changeset
32
cc7909f86841 remvoe TransFinifte1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 422
diff changeset
33
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 open _∧_
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 open _∨_
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 open Bool
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 open _==_
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
40 <_,_> : (x y : HOD) → HOD
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 < x , y > = (x , x ) , (x , y )
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 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
44 exg-pair {x} {y} = record { eq→ = left ; eq← = right } where
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
45 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
46 left (case1 t) = case2 t
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 left (case2 t) = case1 t
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
48 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
49 right (case1 t) = case2 t
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 right (case2 t) = case1 t
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
52 ord≡→≡ : { x y : HOD } → & x ≡ & y → x ≡ y
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
53 ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) *iso *iso ( cong ( λ k → * k ) eq )
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
55 od≡→≡ : { x y : Ordinal } → * x ≡ * y → x ≡ y
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
56 od≡→≡ eq = subst₂ (λ j k → j ≡ k ) &iso &iso ( cong ( λ k → & k ) eq )
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
58 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
59 eq-prod refl refl = refl
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60
410
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 376
diff changeset
61 xx=zy→x=y : {x y z : HOD } → ( x , x ) =h= ( z , y ) → x ≡ y
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
62 xx=zy→x=y {x} {y} eq with trio< (& x) (& y)
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
63 xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c with eq← eq {& y} (case2 refl)
410
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 376
diff changeset
64 xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 376
diff changeset
65 xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 376
diff changeset
66 xx=zy→x=y {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
67 xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c with eq← eq {& y} (case2 refl)
410
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 376
diff changeset
68 xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 376
diff changeset
69 xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 376
diff changeset
70
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
71 prod-eq : { x x' y y' : HOD } → < x , y > =h= < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
72 prod-eq {x} {x'} {y} {y'} eq = ⟪ lemmax , lemmay ⟫ where
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
73 lemma2 : {x y z : HOD } → ( x , x ) =h= ( z , y ) → z ≡ y
410
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 376
diff changeset
74 lemma2 {x} {y} {z} eq = trans (sym (xx=zy→x=y lemma3 )) ( xx=zy→x=y eq ) where
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
75 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
76 lemma3 = ==-trans eq exg-pair
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
77 lemma1 : {x y : HOD } → ( x , x ) =h= ( y , y ) → x ≡ y
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
78 lemma1 {x} {y} eq with eq← eq {& y} (case2 refl)
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 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
80 lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s)
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
81 lemma4 : {x y z : HOD } → ( x , y ) =h= ( x , z ) → y ≡ z
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
82 lemma4 {x} {y} {z} eq with eq← eq {& z} (case2 refl)
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 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
84 ... | refl with lemma2 (==-sym eq )
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 ... | refl = refl
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 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
87 lemmax : x ≡ x'
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
88 lemmax with eq→ eq {& (x , x)} (case1 refl)
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 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
90 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
91 ... | refl = lemma1 (ord→== s )
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 lemmay : y ≡ y'
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 lemmay with lemmax
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 ... | refl with lemma4 eq -- with (x,y)≡(x,y')
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
95 ... | eq1 = lemma4 (ord→== (cong (λ k → & k ) eq1 ))
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
97 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
98 -- unlike ordered pair, ZFProduct is not a HOD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
99
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 data ord-pair : (p : Ordinal) → Set n where
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
101 pair : (x y : Ordinal ) → ord-pair ( & ( < * x , * y > ) )
272
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 ZFProduct : OD
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 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
105
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 -- 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
107 -- 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
108 -- eq-pair refl refl = HE.refl
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110 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
111 pi1 ( pair x y) = x
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
113 π1 : { p : HOD } → def ZFProduct (& p) → HOD
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
114 π1 lt = * (pi1 lt )
272
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 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
117 pi2 ( pair x y ) = y
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
118
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
119 π2 : { p : HOD } → def ZFProduct (& p) → HOD
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
120 π2 lt = * (pi2 lt )
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
122 op-cons : { ox oy : Ordinal } → def ZFProduct (& ( < * ox , * oy > ))
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
123 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
124
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
125 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
126 def-subst df refl refl = df
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
127
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
128 p-cons : ( x y : HOD ) → def ZFProduct (& ( < x , y >))
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
129 p-cons x y = def-subst {_} {_} {ZFProduct} {& (< x , y >)} (pair (& x) ( & y )) refl (
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
130 let open ≡-Reasoning in begin
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
131 & < * (& x) , * (& y) >
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
132 ≡⟨ cong₂ (λ j k → & < j , k >) *iso *iso ⟩
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
133 & < x , y >
329
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
134 ∎ )
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
136 op-iso : { op : Ordinal } → (q : ord-pair op ) → & < * (pi1 q) , * (pi2 q) > ≡ op
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
137 op-iso (pair ox oy) = refl
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
139 p-iso : { x : HOD } → (p : def ZFProduct (& 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
140 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
141
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
142 p-pi1 : { x y : HOD } → (p : def ZFProduct (& < x , y >) ) → π1 p ≡ x
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
143 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
144
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
145 p-pi2 : { x y : HOD } → (p : def ZFProduct (& < x , y >) ) → π2 p ≡ y
272
985a1af11bce separate ordered pair and Boolean Algebra
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
146 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
147
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
148 ω-pair : {x y : HOD} → {m : Ordinal} → & x o< next m → & y o< next m → & (x , y) o< next m
417
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 411
diff changeset
149 ω-pair lx ly = next< (omax<nx lx ly ) ho<
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 411
diff changeset
150
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
151 ω-opair : {x y : HOD} → {m : Ordinal} → & x o< next m → & y o< next m → & < x , y > o< next m
417
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 411
diff changeset
152 ω-opair {x} {y} {m} lx ly = lemma0 where
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
153 lemma0 : & < x , y > o< next m
411
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 410
diff changeset
154 lemma0 = osucprev (begin
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
155 osuc (& < x , y >)
410
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 376
diff changeset
156 <⟨ osuc<nx ho< ⟩
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
157 next (omax (& (x , x)) (& (x , y)))
411
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 410
diff changeset
158 ≡⟨ cong (λ k → next k) (sym ( omax≤ _ _ pair-xx<xy )) ⟩
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
159 next (osuc (& (x , y)))
368
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 367
diff changeset
160 ≡⟨ sym (nexto≡) ⟩
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
161 next (& (x , y))
417
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 411
diff changeset
162 ≤⟨ x<ny→≤next (ω-pair lx ly) ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 411
diff changeset
163 next m
410
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 376
diff changeset
164 ∎ ) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 376
diff changeset
165 open o≤-Reasoning O
367
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 365
diff changeset
166
362
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 361
diff changeset
167 _⊗_ : (A B : HOD) → HOD
376
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 369
diff changeset
168 A ⊗ B = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))
360
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 329
diff changeset
169
417
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 411
diff changeset
170 product→ : {A B a b : HOD} → A ∋ a → B ∋ b → ( A ⊗ B ) ∋ < a , b >
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
171 product→ {A} {B} {a} {b} A∋a B∋b = λ t → t (& (Replace A (λ a → < a , b >)))
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
172 ⟪ lemma1 , subst (λ k → odef k (& < a , b >)) (sym *iso) lemma2 ⟫ where
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
173 lemma1 : odef (Replace B (λ b₁ → Replace A (λ a₁ → < a₁ , b₁ >))) (& (Replace A (λ a₁ → < a₁ , b >)))
417
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 411
diff changeset
174 lemma1 = replacement← B b B∋b
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
175 lemma2 : odef (Replace A (λ a₁ → < a₁ , b >)) (& < a , b >)
417
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 411
diff changeset
176 lemma2 = replacement← A a A∋a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 411
diff changeset
177
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
178 x<nextA : {A x : HOD} → A ∋ x → & x o< next (odmax A)
417
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 411
diff changeset
179 x<nextA {A} {x} A∋x = ordtrans (c<→o< {x} {A} A∋x) ho<
362
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 361
diff changeset
180
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
181 A<Bnext : {A B x : HOD} → & A o< & B → A ∋ x → & x o< next (odmax B)
417
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 411
diff changeset
182 A<Bnext {A} {B} {x} lt A∋x = osucprev (begin
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
183 osuc (& x)
417
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 411
diff changeset
184 <⟨ osucc (c<→o< A∋x) ⟩
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
185 osuc (& A)
417
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 411
diff changeset
186 <⟨ osucc lt ⟩
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
187 osuc (& B)
417
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 411
diff changeset
188 <⟨ osuc<nx ho< ⟩
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 411
diff changeset
189 next (odmax B)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 411
diff changeset
190 ∎ ) where open o≤-Reasoning O
362
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 361
diff changeset
191
417
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 411
diff changeset
192 ZFP : (A B : HOD) → HOD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 411
diff changeset
193 ZFP A B = record { od = record { def = λ x → ord-pair x ∧ ((p : ord-pair x ) → odef A (pi1 p) ∧ odef B (pi2 p) )} ;
418
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
194 odmax = omax (next (odmax A)) (next (odmax B)) ; <odmax = λ {y} px → lemma y px }
417
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 411
diff changeset
195 where
418
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
196 lemma : (y : Ordinal) → ( ord-pair y ∧ ((p : ord-pair y) → odef A (pi1 p) ∧ odef B (pi2 p))) → y o< omax (next (odmax A)) (next (odmax B))
417
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 411
diff changeset
197 lemma y lt with proj1 lt
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
198 lemma p lt | pair x y with trio< (& A) (& B)
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
199 lemma p lt | pair x y | tri< a ¬b ¬c = ordtrans (ω-opair (A<Bnext a (subst (λ k → odef A k ) (sym &iso)
418
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
200 (proj1 (proj2 lt (pair x y))))) (lemma1 (proj2 (proj2 lt (pair x y))))) (omax-y _ _ ) where
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
201 lemma1 : odef B y → & (* y) o< next (HOD.odmax B)
418
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
202 lemma1 lt = x<nextA {B} (d→∋ B lt)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
203 lemma p lt | pair x y | tri≈ ¬a b ¬c = ordtrans (ω-opair (x<nextA {A} (d→∋ A ((proj1 (proj2 lt (pair x y)))))) lemma2 ) (omax-x _ _ ) where
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
204 lemma2 : & (* y) o< next (HOD.odmax A)
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
205 lemma2 = ordtrans ( subst (λ k → & (* y) o< k ) (sym b) (c<→o< (d→∋ B ((proj2 (proj2 lt (pair x y))))))) ho<
418
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
206 lemma p lt | pair x y | tri> ¬a ¬b c = ordtrans (ω-opair (x<nextA {A} (d→∋ A ((proj1 (proj2 lt (pair x y))))))
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
207 (A<Bnext c (subst (λ k → odef B k ) (sym &iso) (proj2 (proj2 lt (pair x y)))))) (omax-x _ _ )
362
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 361
diff changeset
208
420
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 419
diff changeset
209 ZFP⊆⊗ : {A B : HOD} {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
210 ZFP⊆⊗ {A} {B} {px} ⟪ (pair x y) , p2 ⟫ = product→ (d→∋ A (proj1 (p2 (pair x y) ))) (d→∋ B (proj2 (p2 (pair x y) )))
418
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
211
420
53422a8ea836 bijection
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 419
diff changeset
212 -- axiom of choice required
422
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
213 -- ⊗⊆ZFP : {A B x : HOD} → ( A ⊗ B ) ∋ x → def ZFProduct (& x)
44a484f17f26 syntax *, &, ⟪ , ⟫
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 420
diff changeset
214 -- ⊗⊆ZFP {A} {B} {x} lt = subst (λ k → ord-pair (& k )) {!!} op-cons
418
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 417
diff changeset
215