Mercurial > hg > Members > kono > Proof > category
annotate src/ToposEx.agda @ 986:e2e11014b0f8
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 04 Mar 2021 18:51:10 +0900 |
| parents | 949f83b3a8f0 |
| children | bbbe97d2a5ea |
| rev | line source |
|---|---|
| 963 | 1 open import CCC |
| 2 open import Level | |
| 3 open import Category | |
| 4 open import cat-utility | |
| 5 open import HomReasoning | |
| 980 | 6 module ToposEx {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) (t : Topos A c ) (n : ToposNat A (CCC.１ c)) where |
| 963 | 7 |
| 974 | 8 open Topos |
| 9 open Equalizer | |
| 10 open ≈-Reasoning A | |
| 11 open CCC.CCC c | |
| 12 | |
| 963 | 13 |
| 14 -- ○ b | |
| 15 -- b -----------→ 1 | |
| 16 -- | | | |
| 17 -- m | | ⊤ | |
| 18 -- ↓ char m ↓ | |
| 19 -- a -----------→ Ω | |
| 20 -- h | |
| 964 | 21 -- |
| 22 -- Ker t h : Equalizer A h (A [ ⊤ o (○ a) ]) | |
| 963 | 23 |
|
977
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
24 mh=⊤ : {a d : Obj A} (h : Hom A a (Ω t)) (p1 : Hom A d a) (p2 : Hom A d １) (eq : A [ A [ h o p1 ] ≈ A [ ⊤ t o p2 ] ] ) |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
25 → A [ A [ h o p1 ] ≈ A [ A [ ⊤ t o ○ a ] o p1 ] ] |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
26 mh=⊤ {a} {d} h p1 p2 eq = begin |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
27 h o p1 ≈⟨ eq ⟩ |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
28 ⊤ t o p2 ≈⟨ cdr (IsCCC.e2 isCCC) ⟩ |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
29 ⊤ t o (○ d) ≈↑⟨ cdr (IsCCC.e2 isCCC) ⟩ |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
30 ⊤ t o ( ○ a o p1 ) ≈⟨ assoc ⟩ |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
31 (⊤ t o ○ a ) o p1 ∎ |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
32 |
| 986 | 33 ---- |
| 34 -- | |
| 35 -- pull back from h | |
| 36 -- | |
| 974 | 37 topos-pullback : {a : Obj A} → (h : Hom A a (Ω t)) → Pullback A h (⊤ t) |
| 38 topos-pullback {a} h = record { | |
| 963 | 39 ab = equalizer-c (Ker t h) -- b |
| 40 ; π1 = equalizer (Ker t h) -- m | |
| 41 ; π2 = ○ ( equalizer-c (Ker t h) ) -- ○ b | |
| 42 ; isPullback = record { | |
| 43 commute = comm | |
|
977
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
44 ; pullback = λ {d} {p1} {p2} eq → IsEqualizer.k (isEqualizer (Ker t h)) p1 (mh=⊤ h p1 p2 eq ) |
| 964 | 45 ; π1p=π1 = IsEqualizer.ek=h (isEqualizer (Ker t h)) |
| 46 ; π2p=π2 = λ {d} {p1'} {p2'} {eq} → lemma2 eq | |
| 47 ; uniqueness = uniq | |
| 963 | 48 } |
| 974 | 49 } where |
| 50 e2 = IsCCC.e2 isCCC | |
| 963 | 51 comm : A [ A [ h o equalizer (Ker t h) ] ≈ A [ ⊤ t o ○ (equalizer-c (Ker t h)) ] ] |
| 52 comm = begin | |
| 964 | 53 h o equalizer (Ker t h) ≈⟨ IsEqualizer.fe=ge (isEqualizer (Ker t h)) ⟩ |
| 54 (⊤ t o ○ a ) o equalizer (Ker t h) ≈↑⟨ assoc ⟩ | |
| 974 | 55 ⊤ t o (○ a o equalizer (Ker t h)) ≈⟨ cdr e2 ⟩ |
| 963 | 56 ⊤ t o ○ (equalizer-c (Ker t h)) ∎ |
| 964 | 57 lemma2 : {d : Obj A} {p1' : Hom A d a} {p2' : Hom A d １} (eq : A [ A [ h o p1' ] ≈ A [ ⊤ t o p2' ] ] ) |
|
977
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
58 → A [ A [ ○ (equalizer-c (Ker t h)) o IsEqualizer.k (isEqualizer (Ker t h)) p1'(mh=⊤ h p1' p2' eq) ] ≈ p2' ] |
| 964 | 59 lemma2 {d} {p1'} {p2'} eq = begin |
|
977
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
60 ○ (equalizer-c (Ker t h)) o IsEqualizer.k (isEqualizer (Ker t h)) p1'(mh=⊤ h p1' p2' eq) ≈⟨ e2 ⟩ |
| 964 | 61 ○ d ≈↑⟨ e2 ⟩ |
| 62 p2' ∎ | |
| 976 | 63 uniq : {d : Obj A} (p' : Hom A d (equalizer-c (Ker t h))) (π1' : Hom A d a) (π2' : Hom A d １) (eq : A [ A [ h o π1' ] ≈ A [ ⊤ t o π2' ] ]) |
| 64 (π1p=π1' : A [ A [ equalizer (Ker t h) o p' ] ≈ π1' ]) (π2p=π2' : A [ A [ ○ (equalizer-c (Ker t h)) o p' ] ≈ π2' ]) | |
|
977
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
65 → A [ IsEqualizer.k (isEqualizer (Ker t h)) π1' (mh=⊤ h π1' π2' eq) ≈ p' ] |
| 976 | 66 uniq {d} (p') p1' p2' eq pe1 pe2 = begin |
|
977
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
67 IsEqualizer.k (isEqualizer (Ker t h)) p1' (mh=⊤ h p1' p2' eq) ≈⟨ IsEqualizer.uniqueness (isEqualizer (Ker t h)) pe1 ⟩ |
| 964 | 68 p' ∎ |
| 963 | 69 |
| 986 | 70 ---- |
| 71 -- | |
| 72 -- pull back from m | |
| 73 -- | |
| 974 | 74 topos-m-pullback : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m ) → Pullback A (char t m mono ) (⊤ t) |
| 976 | 75 topos-m-pullback {a} {b} m mono = record { |
| 76 ab = b | |
| 77 ; π1 = m | |
| 78 ; π2 = ○ b | |
| 79 ; isPullback = record { | |
| 80 commute = char-m=⊤ t m mono | |
| 978 | 81 ; pullback = λ {d} {p1} {p2} eq → f← o k p1 p2 eq |
|
977
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
82 ; π1p=π1 = λ {d} {p1'} {p2'} {eq} → lemma3 p1' p2' eq |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
83 ; π2p=π2 = λ {d} {p1'} {p2'} {eq} → trans-hom (IsCCC.e2 isCCC) (sym (IsCCC.e2 isCCC)) |
| 979 | 84 ; uniqueness = uniq |
| 976 | 85 } |
| 86 } where | |
| 986 | 87 f← = Iso.≅← (IsoL.iso-L (IsTopos.ker-iso (isTopos t) m mono )) |
| 88 f→ = Iso.≅→ (IsoL.iso-L (IsTopos.ker-iso (isTopos t) m mono )) | |
|
977
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
89 k : {d : Obj A} (p1 : Hom A d a) → (p2 : Hom A d １) → A [ A [ char t m mono o p1 ] ≈ A [ ⊤ t o p2 ] ] → Hom A d (equalizer-c (Ker t (char t m mono))) |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
90 k p1 p2 eq = IsEqualizer.k (isEqualizer (Ker t (char t m mono))) p1 (mh=⊤ (char t m mono) p1 p2 eq ) |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
91 lemma3 : {d : Obj A} (p1 : Hom A d a) → (p2 : Hom A d １) |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
92 → (eq : A [ A [ char t m mono o p1 ] ≈ A [ ⊤ t o p2 ] ] ) → m o (f← o k p1 p2 eq ) ≈ p1 |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
93 lemma3 {d} p1 p2 eq = begin |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
94 m o (f← o k p1 p2 eq ) ≈⟨ assoc ⟩ |
| 986 | 95 (m o f← ) o k p1 p2 eq ≈⟨ car (IsoL.iso≈L (IsTopos.ker-iso (isTopos t) m mono )) ⟩ |
|
977
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
96 equalizer (Ker t (char t m mono)) o k p1 p2 eq ≈⟨ IsEqualizer.ek=h (isEqualizer (Ker t (char t m mono))) ⟩ |
|
8ffdc897f29b
fix Topos equalizer iso
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
976
diff
changeset
|
97 p1 ∎ |
| 978 | 98 uniq : {d : Obj A} (p' : Hom A d b) (π1' : Hom A d a) (π2' : Hom A d １) |
| 99 (eq : A [ A [ char t m mono o π1' ] ≈ A [ ⊤ t o π2' ] ]) → | |
| 100 A [ A [ m o p' ] ≈ π1' ] → A [ A [ ○ b o p' ] ≈ π2' ] → f← o k π1' π2' eq ≈ p' | |
| 101 uniq {d} p p1 p2 eq pe1 pe2 = begin | |
| 979 | 102 f← o k p1 p2 eq ≈⟨ cdr ( IsEqualizer.uniqueness (isEqualizer (Ker t (char t m mono))) lemma4) ⟩ |
| 103 f← o (f→ o p ) ≈⟨ assoc ⟩ | |
| 986 | 104 (f← o f→ ) o p ≈⟨ car (Iso.iso→ (IsoL.iso-L (IsTopos.ker-iso (isTopos t) m mono ))) ⟩ |
| 979 | 105 id1 A _ o p ≈⟨ idL ⟩ |
| 106 p ∎ where | |
| 107 lemma4 : A [ A [ equalizer (Ker t (char t m mono)) o (f→ o p) ] ≈ p1 ] | |
| 108 lemma4 = begin | |
| 109 equalizer (Ker t (char t m mono)) o (f→ o p) ≈⟨ assoc ⟩ | |
| 986 | 110 (equalizer (Ker t (char t m mono)) o f→ ) o p ≈⟨ car (IsoL.L≈iso (IsTopos.ker-iso (isTopos t) m mono )) ⟩ |
| 979 | 111 m o p ≈⟨ pe1 ⟩ |
| 112 p1 ∎ where | |
| 978 | 113 |
| 965 | 114 |
| 971 | 115 δmono : {b : Obj A } → Mono A < id1 A b , id1 A b > |
| 116 δmono = record { | |
| 117 isMono = m1 | |
| 118 } where | |
| 119 m1 : {d b : Obj A} (f g : Hom A d b) → A [ A [ < id1 A b , id1 A b > o f ] ≈ A [ < id1 A b , id1 A b > o g ] ] → A [ f ≈ g ] | |
| 972 | 120 m1 {d} {b} f g eq = begin |
| 121 f ≈↑⟨ idL ⟩ | |
| 122 id1 A _ o f ≈↑⟨ car (IsCCC.e3a isCCC) ⟩ | |
| 123 (π o < id1 A b , id1 A b >) o f ≈↑⟨ assoc ⟩ | |
| 124 π o (< id1 A b , id1 A b > o f) ≈⟨ cdr eq ⟩ | |
| 125 π o (< id1 A b , id1 A b > o g) ≈⟨ assoc ⟩ | |
| 126 (π o < id1 A b , id1 A b >) o g ≈⟨ car (IsCCC.e3a isCCC) ⟩ | |
| 127 id1 A _ o g ≈⟨ idL ⟩ | |
| 128 g ∎ | |
| 965 | 129 |
| 984 | 130 -- |
| 986 | 131 -- |
| 132 -- Hom equality and Ω | |
| 133 -- | |
| 134 -- | |
| 984 | 135 -- a -----------→ + |
| 136 -- f||g ○ a | | |
| 137 -- ↓↓ | | |
| 138 -- b -----------→ 1 | |
| 139 -- | ○ b | | |
| 140 -- <1,1> | | ⊤ | |
| 141 -- ↓ ↓ | |
| 142 -- b ∧ b ---------→ Ω | |
| 143 -- char <1,1> | |
| 144 | |
| 971 | 145 prop32→ : {a b : Obj A}→ (f g : Hom A a b ) |
| 146 → A [ f ≈ g ] → A [ A [ char t < id1 A b , id1 A b > δmono o < f , g > ] ≈ A [ ⊤ t o ○ a ] ] | |
| 972 | 147 prop32→ {a} {b} f g f=g = begin |
| 148 char t < id1 A b , id1 A b > δmono o < f , g > ≈⟨ cdr ( IsCCC.π-cong isCCC refl-hom (sym f=g)) ⟩ | |
| 149 char t < id1 A b , id1 A b > δmono o < f , f > ≈↑⟨ cdr ( IsCCC.π-cong isCCC idL idL ) ⟩ | |
| 150 char t < id1 A b , id1 A b > δmono o < id1 A _ o f , id1 A _ o f > ≈↑⟨ cdr ( IsCCC.distr-π isCCC ) ⟩ | |
| 151 char t < id1 A b , id1 A b > δmono o (< id1 A _ , id1 A _ > o f) ≈⟨ assoc ⟩ | |
| 975 | 152 (char t < id1 A b , id1 A b > δmono o < id1 A b , id1 A b > ) o f ≈⟨ car (char-m=⊤ t < id1 A b , id1 A b > δmono ) ⟩ |
| 972 | 153 (⊤ t o ○ b) o f ≈↑⟨ assoc ⟩ |
| 154 ⊤ t o (○ b o f) ≈⟨ cdr (IsCCC.e2 isCCC) ⟩ | |
| 975 | 155 ⊤ t o ○ a ∎ |
| 971 | 156 |
| 157 prop23→ : {a b : Obj A}→ (f g : Hom A a b ) | |
| 158 → A [ A [ char t < id1 A b , id1 A b > δmono o < f , g > ] ≈ A [ ⊤ t o ○ a ] ] → A [ f ≈ g ] | |
| 979 | 159 prop23→ {a} {b} f g eq = begin |
| 160 f ≈⟨ IsCCC.π≈ isCCC p2 ⟩ | |
| 161 k ≈↑⟨ IsCCC.π'≈ isCCC p2 ⟩ | |
| 162 g ∎ | |
| 163 where | |
| 976 | 164 δb : Hom A ( b ∧ b ) (Ω t) |
| 165 δb = char t < id1 A b , id1 A b > δmono | |
| 166 ip : Pullback A δb (⊤ t) | |
| 167 ip = topos-m-pullback < id1 A b , id1 A b > δmono | |
| 168 k : Hom A a b | |
| 169 k = IsPullback.pullback (Pullback.isPullback ip ) eq | |
| 979 | 170 p2 : < f , g > ≈ < k , k > |
| 976 | 171 p2 = begin |
| 979 | 172 < f , g > ≈↑⟨ IsPullback.π1p=π1 (Pullback.isPullback ip) ⟩ |
| 173 < id1 A b , id1 A b > o k ≈⟨ IsCCC.distr-π isCCC ⟩ | |
| 174 < id1 A b o k , id1 A b o k > ≈⟨ IsCCC.π-cong isCCC idL idL ⟩ | |
| 175 < k , k > ∎ | |
| 986 | 176 -- |
| 177 -- | |
| 178 -- Initial Natural number diagram | |
| 179 -- | |
| 180 -- | |
| 971 | 181 |
| 980 | 182 open NatD |
| 183 open ToposNat n | |
| 971 | 184 |
| 984 | 185 -- 0 suc |
| 186 -- 1 -----------→ N ---------→ N | |
| 187 -- | | | | |
| 188 -- | <f,g> | <f,g>| | |
| 189 -- | ↓ ↓ | |
| 190 -- 1 ---------→ N x A -----→ N x A | |
| 191 -- <0,z> <suc o π , h > | |
| 192 | |
| 980 | 193 N : Obj A |
| 986 | 194 N = Nat iNat |
| 980 | 195 |
| 196 record prop33 {a : Obj A} (f : Hom A １ a ) ( h : Hom A (N ∧ a) a ) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where | |
| 971 | 197 field |
| 980 | 198 g : Hom A N a |
| 986 | 199 g0=f : A [ A [ g o nzero iNat ] ≈ f ] |
| 200 gs=h : A [ A [ g o nsuc iNat ] ≈ A [ h o < id1 A _ , g > ] ] | |
| 982 | 201 xnat : NatD A １ |
| 979 | 202 |
| 980 | 203 p33 : {a : Obj A} (z : Hom A １ a ) ( h : Hom A (N ∧ a) a ) → prop33 z h |
| 204 p33 {a} z h = record { | |
| 205 g = g | |
| 206 ; g0=f = iii | |
| 207 ; gs=h = v | |
| 982 | 208 ; xnat = xnat |
| 980 | 209 } where |
| 210 xnat : NatD A １ | |
| 986 | 211 xnat = record { Nat = N ∧ a ; nzero = < nzero iNat , z > ; nsuc = < nsuc iNat o π , h > } |
| 980 | 212 fg : Hom A N (N ∧ a ) |
| 986 | 213 fg = initialNat xnat -- < f , g > |
| 980 | 214 f : Hom A N N |
| 215 f = π o fg | |
| 216 g : Hom A N a | |
| 217 g = π' o fg | |
| 986 | 218 i : f o nzero iNat ≈ nzero iNat |
| 980 | 219 i = begin |
| 986 | 220 f o nzero iNat ≈⟨⟩ |
| 221 (π o fg) o nzero iNat ≈↑⟨ assoc ⟩ | |
| 222 π o (fg o nzero iNat ) ≈⟨ cdr (IsToposNat.izero isToposN xnat ) ⟩ | |
| 982 | 223 π o nzero xnat ≈⟨ IsCCC.e3a isCCC ⟩ |
| 986 | 224 nzero iNat ∎ |
| 225 ii : f o nsuc iNat ≈ nsuc iNat o f | |
| 980 | 226 ii = begin |
| 986 | 227 f o nsuc iNat ≈⟨⟩ |
| 228 (π o fg ) o nsuc iNat ≈↑⟨ assoc ⟩ | |
| 229 π o ( fg o nsuc iNat ) ≈⟨ cdr (IsToposNat.isuc isToposN xnat ) ⟩ | |
| 230 π o (nsuc xnat o initialNat xnat) ≈⟨ assoc ⟩ | |
| 231 (π o < nsuc iNat o π , h > ) o initialNat xnat ≈⟨ car (IsCCC.e3a isCCC) ⟩ | |
| 232 ( nsuc iNat o π ) o initialNat xnat ≈↑⟨ assoc ⟩ | |
| 233 nsuc iNat o ( π o initialNat xnat ) ≈⟨⟩ | |
| 234 nsuc iNat o f ∎ | |
| 982 | 235 ig : f ≈ id1 A N |
| 236 ig = begin | |
| 986 | 237 f ≈⟨ nat-unique iNat i ii ⟩ |
| 238 initialNat iNat ≈↑⟨ nat-unique iNat idL (trans-hom idL (sym idR) ) ⟩ | |
| 982 | 239 id1 A _ ∎ |
| 986 | 240 iii : g o nzero iNat ≈ z |
| 980 | 241 iii = begin |
| 986 | 242 g o nzero iNat ≈⟨⟩ (π' o initialNat xnat ) o nzero iNat ≈↑⟨ assoc ⟩ |
| 243 π' o ( initialNat xnat o nzero iNat) ≈⟨ cdr (IsToposNat.izero isToposN xnat) ⟩ | |
| 244 π' o < nzero iNat , z > ≈⟨ IsCCC.e3b isCCC ⟩ | |
| 980 | 245 z ∎ |
| 986 | 246 iv : g o nsuc iNat ≈ h o < f , g > |
| 980 | 247 iv = begin |
| 986 | 248 g o nsuc iNat ≈⟨⟩ |
| 249 (π' o initialNat xnat) o nsuc iNat ≈↑⟨ assoc ⟩ | |
| 250 π' o (initialNat xnat o nsuc iNat ) ≈⟨ cdr (IsToposNat.isuc isToposN xnat) ⟩ | |
| 251 π' o (nsuc xnat o initialNat xnat ) ≈⟨ assoc ⟩ | |
| 252 (π' o nsuc xnat ) o initialNat xnat ≈⟨ car (IsCCC.e3b isCCC) ⟩ | |
| 253 h o initialNat xnat ≈↑⟨ cdr (IsCCC.e3c isCCC) ⟩ | |
| 980 | 254 h o < π o fg , π' o fg > ≈⟨⟩ |
| 255 h o < f , g > ∎ | |
| 986 | 256 v : A [ A [ g o nsuc iNat ] ≈ A [ h o < id1 A N , g > ] ] |
| 980 | 257 v = begin |
| 986 | 258 g o nsuc iNat ≈⟨ iv ⟩ |
| 980 | 259 h o < f , g > ≈⟨ cdr ( IsCCC.π-cong isCCC ig refl-hom) ⟩ |
| 260 h o < id1 A N , g > ∎ | |
| 261 | |
| 984 | 262 -- . |
| 263 -- / | \ | |
| 264 -- / | \ | |
| 265 -- / ↓ \ | |
| 266 -- N --→ N ←-- a | |
| 267 -- | |
| 986 | 268 cor33 : coProduct A １ (Nat iNat ) -- N ≅ N + 1 |
| 980 | 269 cor33 = record { |
| 270 coproduct = N | |
| 986 | 271 ; κ1 = nzero iNat |
| 272 ; κ2 = nsuc iNat | |
| 971 | 273 ; isProduct = record { |
| 980 | 274 _+_ = λ {a} f g → prop33.g (p f ( g o π )) -- Hom A (N n ∧ a) a |
| 275 ; κ1f+g=f = λ {a} {f} {g} → prop33.g0=f (p f (g o π ) ) | |
| 276 ; κ2f+g=g = λ {a} {f} {g} → k2 {a} {f} {g} | |
| 982 | 277 ; uniqueness = uniq |
| 983 | 278 ; +-cong = pcong |
| 971 | 279 } |
| 972 | 280 } where |
| 980 | 281 p : {a : Obj A} (f : Hom A １ a) ( h : Hom A (N ∧ a) a ) → prop33 f h |
| 282 p f h = p33 f h | |
| 986 | 283 k2 : {a : Obj A} {f : Hom A １ a} {g : Hom A (Nat iNat) a } |
| 284 → A [ A [ prop33.g (p f (g o π)) o nsuc iNat ] ≈ g ] | |
| 972 | 285 k2 {a} {f} {g} = begin |
| 986 | 286 (prop33.g (p f (g o π)) o nsuc iNat) ≈⟨ prop33.gs=h (p f (g o π )) ⟩ |
| 980 | 287 ( g o π ) o < id1 A N , prop33.g (p f (g o π)) > ≈⟨ sym assoc ⟩ |
| 288 g o ( π o < id1 A N , prop33.g (p f (g o π)) >) ≈⟨ cdr (IsCCC.e3a isCCC ) ⟩ | |
| 289 g o id1 A N ≈⟨ idR ⟩ | |
| 972 | 290 g ∎ |
| 986 | 291 pp : {c : Obj A} {h : Hom A (Nat iNat) c} → prop33 ( h o nzero iNat ) ( (h o nsuc iNat) o π) |
| 292 pp {c} {h} = p ( h o nzero iNat ) ( (h o nsuc iNat) o π) | |
| 293 uniq : {c : Obj A} {h : Hom A (Nat iNat) c} → | |
| 982 | 294 prop33.g pp ≈ h |
| 295 uniq {c} {h} = begin | |
| 983 | 296 prop33.g pp ≈⟨⟩ |
| 986 | 297 π' o initialNat (prop33.xnat pp) ≈↑⟨ cdr (nat-unique (prop33.xnat pp) ( |
| 983 | 298 begin |
| 986 | 299 < id1 A _ , h > o nzero iNat ≈⟨ IsCCC.distr-π isCCC ⟩ |
| 300 < id1 A _ o nzero iNat , h o nzero iNat > ≈⟨ IsCCC.π-cong isCCC idL refl-hom ⟩ | |
| 301 < nzero iNat , h o nzero iNat > ≈⟨⟩ | |
| 983 | 302 nzero (prop33.xnat pp) ∎ ) |
| 303 (begin | |
| 986 | 304 < id1 A _ , h > o nsuc iNat ≈⟨ IsCCC.distr-π isCCC ⟩ |
| 305 < id1 A _ o nsuc iNat , h o nsuc iNat > ≈⟨ IsCCC.π-cong isCCC idL refl-hom ⟩ | |
| 306 < nsuc iNat , h o nsuc iNat > ≈↑⟨ IsCCC.π-cong isCCC idR idR ⟩ | |
| 307 < nsuc iNat o id1 A _ , (h o nsuc iNat ) o id1 A _ > ≈↑⟨ IsCCC.π-cong isCCC (cdr (IsCCC.e3a isCCC)) (cdr (IsCCC.e3a isCCC)) ⟩ | |
| 308 < nsuc iNat o ( π o < id1 A _ , h > ) , (h o nsuc iNat ) o ( π o < id1 A _ , h > ) > ≈⟨ IsCCC.π-cong isCCC assoc assoc ⟩ | |
| 309 < (nsuc iNat o π ) o < id1 A _ , h > , ((h o nsuc iNat ) o π ) o < id1 A _ , h > > ≈↑⟨ IsCCC.distr-π isCCC ⟩ | |
| 310 < nsuc iNat o π , (h o nsuc iNat ) o π > o < id1 A _ , h > ≈⟨⟩ | |
| 983 | 311 nsuc (prop33.xnat pp) o < id1 A _ , h > ∎ )) ⟩ |
| 312 π' o < id1 A _ , h > ≈⟨ IsCCC.e3b isCCC ⟩ | |
| 982 | 313 h ∎ |
| 986 | 314 pcong : {a : Obj A } {f f' : Hom A １ a } {g g' : Hom A (Nat iNat) a } → (f=f' : f ≈ f' ) → ( g=g' : g ≈ g' ) |
| 983 | 315 → prop33.g (p f (g o π)) ≈ prop33.g (p f' (g' o π)) |
| 316 pcong {a} {f} {f'} {g} {g'} f=f' g=g' = begin | |
| 317 prop33.g (p f (g o π)) ≈⟨⟩ | |
| 986 | 318 π' o (initialNat (prop33.xnat (p f (g o π)))) ≈↑⟨ cdr (nat-unique (prop33.xnat (p f (g o π))) lem1 lem2 ) ⟩ |
| 319 π' o (initialNat (prop33.xnat (p f' (g' o π)))) ≈⟨⟩ | |
| 983 | 320 prop33.g (p f' (g' o π)) ∎ where |
| 986 | 321 lem1 : A [ A [ initialNat (prop33.xnat (p f' ((A Category.o g') π))) o nzero iNat ] ≈ nzero (prop33.xnat (p f ((A Category.o g) π))) ] |
| 983 | 322 lem1 = begin |
| 986 | 323 initialNat (prop33.xnat (p f' (g' o π))) o nzero iNat ≈⟨ IsToposNat.izero isToposN _ ⟩ |
| 983 | 324 nzero (prop33.xnat (p f' (g' o π))) ≈⟨⟩ |
| 986 | 325 < nzero iNat , f' > ≈⟨ IsCCC.π-cong isCCC refl-hom (sym f=f') ⟩ |
| 326 < nzero iNat , f > ≈⟨⟩ | |
| 983 | 327 nzero (prop33.xnat (p f (g o π))) ∎ |
| 986 | 328 lem2 : A [ A [ initialNat (prop33.xnat (p f' (g' o π))) o nsuc iNat ] ≈ A [ nsuc (prop33.xnat (p f (g o π))) o initialNat (prop33.xnat (p f' (g' o π))) ] ] |
| 983 | 329 lem2 = begin |
| 986 | 330 initialNat (prop33.xnat (p f' (g' o π))) o nsuc iNat ≈⟨ IsToposNat.isuc isToposN _ ⟩ |
| 331 nsuc (prop33.xnat (p f' (g' o π))) o initialNat (prop33.xnat (p f' (g' o π))) ≈⟨⟩ | |
| 332 < (nsuc iNat) o π , g' o π > o initialNat (prop33.xnat (p f' (g' o π))) ≈⟨ car ( IsCCC.π-cong isCCC refl-hom (car (sym g=g')) ) ⟩ | |
| 333 < (nsuc iNat) o π , g o π > o initialNat (prop33.xnat (p f' (g' o π))) ≈⟨⟩ | |
| 334 nsuc (prop33.xnat (p f (g o π))) o initialNat (prop33.xnat (p f' (g' o π))) ∎ |