Mercurial > hg > Members > kono > Proof > category
annotate src/CCC.agda @ 1110:45de2b31bf02
add original library and fix for safe mode
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 07 Oct 2023 19:43:31 +0900 |
| parents | 321f0fef54c2 |
| children |
| rev | line source |
|---|---|
|
1110
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1097
diff
changeset
|
1 {-# OPTIONS --cubical-compatible --safe #-} |
|
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1097
diff
changeset
|
2 |
| 779 | 3 open import Level |
| 950 | 4 open import Category |
| 779 | 5 module CCC where |
| 6 | |
| 950 | 7 |
| 779 | 8 open import HomReasoning |
|
1110
45de2b31bf02
add original library and fix for safe mode
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1097
diff
changeset
|
9 open import Definitions |
| 780 | 10 open import Relation.Binary.PropositionalEquality |
| 779 | 11 |
| 783 | 12 |
| 13 open import HomReasoning | |
| 14 | |
| 784 | 15 record IsCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) |
| 783 | 16 ( １ : Obj A ) |
| 17 ( ○ : (a : Obj A ) → Hom A a １ ) | |
| 18 ( _∧_ : Obj A → Obj A → Obj A ) | |
| 19 ( <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b) ) | |
| 20 ( π : {a b : Obj A } → Hom A (a ∧ b) a ) | |
| 21 ( π' : {a b : Obj A } → Hom A (a ∧ b) b ) | |
| 22 ( _<=_ : (a b : Obj A ) → Obj A ) | |
| 23 ( _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) ) | |
| 24 ( ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a ) | |
| 25 : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where | |
| 26 field | |
| 27 -- cartesian | |
| 793 | 28 e2 : {a : Obj A} → ∀ { f : Hom A a １ } → A [ f ≈ ○ a ] |
| 783 | 29 e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π o < f , g > ] ≈ f ] |
| 30 e3b : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π' o < f , g > ] ≈ g ] | |
| 31 e3c : {a b c : Obj A} → { h : Hom A c (a ∧ b) } → A [ < A [ π o h ] , A [ π' o h ] > ≈ h ] | |
| 785 | 32 π-cong : {a b c : Obj A} → { f f' : Hom A c a }{ g g' : Hom A c b } → A [ f ≈ f' ] → A [ g ≈ g' ] → A [ < f , g > ≈ < f' , g' > ] |
| 783 | 33 -- closed |
| 34 e4a : {a b c : Obj A} → { h : Hom A (c ∧ b) a } → A [ A [ ε o < A [ (h *) o π ] , π' > ] ≈ h ] | |
| 35 e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o < A [ k o π ] , π' > ] ) * ≈ k ] | |
| 787 | 36 *-cong : {a b c : Obj A} → { f f' : Hom A (a ∧ b) c } → A [ f ≈ f' ] → A [ f * ≈ f' * ] |
| 967 | 37 open ≈-Reasoning A |
| 38 e'2 : ○ １ ≈ id1 A １ | |
| 39 e'2 = begin | |
| 783 | 40 ○ １ |
| 793 | 41 ≈↑⟨ e2 ⟩ |
| 783 | 42 id1 A １ |
| 43 ∎ | |
| 967 | 44 e''2 : {a b : Obj A} {f : Hom A a b } → ( ○ b o f ) ≈ ○ a |
| 45 e''2 {a} {b} {f} = begin | |
| 783 | 46 ○ b o f |
| 793 | 47 ≈⟨ e2 ⟩ |
| 783 | 48 ○ a |
| 49 ∎ | |
| 967 | 50 π-id : {a b : Obj A} → < π , π' > ≈ id1 A (a ∧ b ) |
| 51 π-id {a} {b} = begin | |
| 789 | 52 < π , π' > |
| 53 ≈↑⟨ π-cong idR idR ⟩ | |
| 54 < π o id1 A (a ∧ b) , π' o id1 A (a ∧ b) > | |
| 55 ≈⟨ e3c ⟩ | |
| 56 id1 A (a ∧ b ) | |
| 57 ∎ | |
| 967 | 58 distr-π : {a b c d : Obj A} {f : Hom A c a }{g : Hom A c b } {h : Hom A d c } → ( < f , g > o h ) ≈ < ( f o h ) , ( g o h ) > |
| 59 distr-π {a} {b} {c} {d} {f} {g} {h} = begin | |
| 783 | 60 < f , g > o h |
| 61 ≈↑⟨ e3c ⟩ | |
| 62 < π o < f , g > o h , π' o < f , g > o h > | |
| 785 | 63 ≈⟨ π-cong assoc assoc ⟩ |
| 64 < ( π o < f , g > ) o h , (π' o < f , g > ) o h > | |
| 65 ≈⟨ π-cong (car e3a ) (car e3b) ⟩ | |
| 783 | 66 < f o h , g o h > |
| 67 ∎ | |
| 794 | 68 _×_ : { a b c d : Obj A } ( f : Hom A a c ) (g : Hom A b d ) → Hom A (a ∧ b) ( c ∧ d ) |
| 967 | 69 f × g = < ( f o π ) , (g o π' ) > |
| 70 π-exchg : {a b c : Obj A} {f : Hom A c a }{g : Hom A c b } → < π' , π > o < f , g > ≈ < g , f > | |
| 71 π-exchg {a} {b} {c} {f} {g} = begin | |
| 72 < π' , π > o < f , g > | |
| 73 ≈⟨ distr-π ⟩ | |
| 74 < π' o < f , g > , π o < f , g > > | |
| 75 ≈⟨ π-cong e3b e3a ⟩ | |
| 76 < g , f > | |
| 77 ∎ | |
| 78 π'π : {a b : Obj A} → < π' , π > o < π' , π > ≈ id1 A (a ∧ b) | |
| 79 π'π = trans-hom π-exchg π-id | |
| 80 exchg-π : {a b c d : Obj A} {f : Hom A c a }{g : Hom A d b } → < f o π , g o π' > o < π' , π > ≈ < f o π' , g o π > | |
| 81 exchg-π {a} {b} {c} {d} {f} {g} = begin | |
| 82 < f o π , g o π' > o < π' , π > | |
| 83 ≈⟨ distr-π ⟩ | |
| 84 < (f o π) o < π' , π > , (g o π' ) o < π' , π > > | |
| 85 ≈↑⟨ π-cong assoc assoc ⟩ | |
| 86 < f o (π o < π' , π > ) , g o (π' o < π' , π >)> | |
| 87 ≈⟨ π-cong (cdr e3a) (cdr e3b) ⟩ | |
| 88 < f o π' , g o π > | |
| 89 ∎ | |
| 979 | 90 π≈ : {a b c : Obj A} {f f' : Hom A c a }{g g' : Hom A c b } → < f , g > ≈ < f' , g' > → f ≈ f' |
| 91 π≈ {_} {_} {_} {f} {f'} {g} {g'} eq = begin | |
| 92 f ≈↑⟨ e3a ⟩ | |
| 93 π o < f , g > ≈⟨ cdr eq ⟩ | |
| 94 π o < f' , g' > ≈⟨ e3a ⟩ | |
| 95 f' | |
| 96 ∎ | |
| 97 π'≈ : {a b c : Obj A} {f f' : Hom A c a }{g g' : Hom A c b } → < f , g > ≈ < f' , g' > → g ≈ g' | |
| 98 π'≈ {_} {_} {_} {f} {f'} {g} {g'} eq = begin | |
| 99 g ≈↑⟨ e3b ⟩ | |
| 100 π' o < f , g > ≈⟨ cdr eq ⟩ | |
| 101 π' o < f' , g' > ≈⟨ e3b ⟩ | |
| 102 g' | |
| 103 ∎ | |
| 967 | 104 distr-* : {a b c d : Obj A } { h : Hom A (a ∧ b) c } { k : Hom A d a } → ( h * o k ) ≈ ( h o < ( k o π ) , π' > ) * |
| 794 | 105 distr-* {a} {b} {c} {d} {h} {k} = begin |
| 106 h * o k | |
| 107 ≈↑⟨ e4b ⟩ | |
| 108 ( ε o < (h * o k ) o π , π' > ) * | |
| 109 ≈⟨ *-cong ( begin | |
| 110 ε o < (h * o k ) o π , π' > | |
| 111 ≈↑⟨ cdr ( π-cong assoc refl-hom ) ⟩ | |
| 112 ε o ( < h * o ( k o π ) , π' > ) | |
| 113 ≈↑⟨ cdr ( π-cong (cdr e3a) e3b ) ⟩ | |
| 114 ε o ( < h * o ( π o < k o π , π' > ) , π' o < k o π , π' > > ) | |
| 115 ≈⟨ cdr ( π-cong assoc refl-hom) ⟩ | |
| 116 ε o ( < (h * o π) o < k o π , π' > , π' o < k o π , π' > > ) | |
| 117 ≈↑⟨ cdr ( distr-π ) ⟩ | |
| 118 ε o ( < h * o π , π' > o < k o π , π' > ) | |
| 119 ≈⟨ assoc ⟩ | |
| 120 ( ε o < h * o π , π' > ) o < k o π , π' > | |
| 121 ≈⟨ car e4a ⟩ | |
| 122 h o < k o π , π' > | |
| 123 ∎ ) ⟩ | |
| 124 ( h o < k o π , π' > ) * | |
| 967 | 125 ∎ |
| 794 | 126 α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) ) |
| 967 | 127 α = < ( π o π ) , < ( π' o π ) , π' > > |
| 794 | 128 α' : {a b c : Obj A } → Hom A ( a ∧ ( b ∧ c ) ) (( a ∧ b ) ∧ c ) |
| 967 | 129 α' = < < π , ( π o π' ) > , ( π' o π' ) > |
| 130 β : {a b c d : Obj A } { f : Hom A a b} { g : Hom A a c } { h : Hom A a d } → ( α o < < f , g > , h > ) ≈ < f , < g , h > > | |
| 794 | 131 β {a} {b} {c} {d} {f} {g} {h} = begin |
| 132 α o < < f , g > , h > | |
| 133 ≈⟨⟩ | |
| 134 ( < ( π o π ) , < ( π' o π ) , π' > > ) o < < f , g > , h > | |
| 135 ≈⟨ distr-π ⟩ | |
| 136 < ( ( π o π ) o < < f , g > , h > ) , ( < ( π' o π ) , π' > o < < f , g > , h > ) > | |
| 137 ≈⟨ π-cong refl-hom distr-π ⟩ | |
| 138 < ( ( π o π ) o < < f , g > , h > ) , ( < ( ( π' o π ) o < < f , g > , h > ) , ( π' o < < f , g > , h > ) > ) > | |
| 139 ≈↑⟨ π-cong assoc ( π-cong assoc refl-hom ) ⟩ | |
| 140 < ( π o (π o < < f , g > , h >) ) , ( < ( π' o ( π o < < f , g > , h > ) ) , ( π' o < < f , g > , h > ) > ) > | |
| 141 ≈⟨ π-cong (cdr e3a ) ( π-cong (cdr e3a ) e3b ) ⟩ | |
| 142 < ( π o < f , g > ) , < ( π' o < f , g > ) , h > > | |
| 143 ≈⟨ π-cong e3a ( π-cong e3b refl-hom ) ⟩ | |
| 144 < f , < g , h > > | |
| 967 | 145 ∎ |
| 794 | 146 |
| 783 | 147 |
| 784 | 148 record CCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where |
| 781 | 149 field |
| 783 | 150 １ : Obj A |
| 151 ○ : (a : Obj A ) → Hom A a １ | |
| 152 _∧_ : Obj A → Obj A → Obj A | |
| 153 <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b) | |
| 154 π : {a b : Obj A } → Hom A (a ∧ b) a | |
| 155 π' : {a b : Obj A } → Hom A (a ∧ b) b | |
| 156 _<=_ : (a b : Obj A ) → Obj A | |
| 157 _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) | |
| 158 ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a | |
| 784 | 159 isCCC : IsCCC A １ ○ _∧_ <_,_> π π' _<=_ _* ε |
| 781 | 160 |
| 1011 | 161 open Functor |
| 162 | |
| 163 record CCCFunctor {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') | |
| 164 (ca : CCC A) (cb : CCC B) (functor : Functor A B) | |
| 165 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ')) where | |
| 166 field | |
| 167 f１ : FObj functor (CCC.１ ca) ≡ CCC.１ cb | |
| 168 f○ : {a : Obj A} → B [ FMap functor (CCC.○ ca a) ≈ | |
| 169 subst (λ k → Hom B (FObj functor a) k) (sym f１) (CCC.○ cb (FObj functor a)) ] | |
| 170 f∧ : {a b : Obj A} → FObj functor ( CCC._∧_ ca a b ) ≡ CCC._∧_ cb (FObj functor a ) (FObj functor b) | |
| 171 f<= : {a b : Obj A} → FObj functor ( CCC._<=_ ca a b ) ≡ CCC._<=_ cb (FObj functor a ) (FObj functor b) | |
| 172 f<> : {a b c : Obj A} → (f : Hom A c a ) → (g : Hom A c b ) | |
| 173 → B [ FMap functor (CCC.<_,_> ca f g ) ≈ | |
| 174 subst (λ k → Hom B (FObj functor c) k ) (sym f∧ ) ( CCC.<_,_> cb (FMap functor f ) ( FMap functor g )) ] | |
| 175 fπ : {a b : Obj A} → B [ FMap functor (CCC.π ca {a} {b}) ≈ | |
| 176 subst (λ k → Hom B k (FObj functor a) ) (sym f∧ ) (CCC.π cb {FObj functor a} {FObj functor b}) ] | |
| 177 fπ' : {a b : Obj A} → B [ FMap functor (CCC.π' ca {a} {b}) ≈ | |
| 178 subst (λ k → Hom B k (FObj functor b) ) (sym f∧ ) (CCC.π' cb {FObj functor a} {FObj functor b}) ] | |
| 179 f* : {a b c : Obj A} → (f : Hom A (CCC._∧_ ca a b) c ) → B [ FMap functor (CCC._* ca f) ≈ | |
| 180 subst (λ k → Hom B (FObj functor a) k) (sym f<=) (CCC._* cb ((subst (λ k → Hom B k (FObj functor c) ) f∧ (FMap functor f) ))) ] | |
| 181 fε : {a b : Obj A} → B [ FMap functor (CCC.ε ca {a} {b} ) | |
| 182 ≈ subst (λ k → Hom B k (FObj functor a)) (trans (cong (λ k → CCC._∧_ cb k (FObj functor b)) (sym f<=)) (sym f∧)) | |
| 183 (CCC.ε cb {FObj functor a} {FObj functor b}) ] | |
| 184 | |
| 950 | 185 open Equalizer |
| 963 | 186 open import equalizer |
| 950 | 187 |
| 952 | 188 record Mono {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {b a : Obj A} (mono : Hom A b a) : Set (c₁ ⊔ c₂ ⊔ ℓ) where |
| 189 field | |
| 190 isMono : {c : Obj A} ( f g : Hom A c b ) → A [ A [ mono o f ] ≈ A [ mono o g ] ] → A [ f ≈ g ] | |
| 191 | |
| 192 open Mono | |
| 193 | |
| 1075 | 194 eMonic : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {b a : Obj A} { f g : Hom A b a } → (equ : Equalizer A f g ) → Mono A (equalizer equ) |
| 195 eMonic A equ = record { isMono = λ f g → monic equ } | |
| 196 | |
| 1069 | 197 iso-mono : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b c : Obj A } {m : Hom A a b} ( mono : Mono A m ) (i : Iso A a c ) → Mono A (A [ m o Iso.≅← i ] ) |
| 198 iso-mono A {a} {b} {c} {m} mono i = record { isMono = λ {d} f g → im f g } where | |
| 199 im : {d : Obj A} (f g : Hom A d c ) → A [ A [ A [ m o Iso.≅← i ] o f ] ≈ A [ A [ m o Iso.≅← i ] o g ] ] → A [ f ≈ g ] | |
| 200 im {d} f g mf=mg = begin | |
| 201 f ≈↑⟨ idL ⟩ | |
| 202 id1 A _ o f ≈↑⟨ car (Iso.iso← i) ⟩ | |
| 203 ( Iso.≅→ i o Iso.≅← i) o f ≈↑⟨ assoc ⟩ | |
| 204 Iso.≅→ i o (Iso.≅← i o f) ≈⟨ cdr ( Mono.isMono mono _ _ (if=ig mf=mg) ) ⟩ | |
| 205 Iso.≅→ i o (Iso.≅← i o g) ≈⟨ assoc ⟩ | |
| 206 ( Iso.≅→ i o Iso.≅← i) o g ≈⟨ car (Iso.iso← i) ⟩ | |
| 207 id1 A _ o g ≈⟨ idL ⟩ | |
| 208 g ∎ where | |
| 209 open ≈-Reasoning A | |
| 210 if=ig : ( m o Iso.≅← i ) o f ≈ ( m o Iso.≅← i ) o g → m o (Iso.≅← i o f ) ≈ m o ( Iso.≅← i o g ) | |
| 211 if=ig eq = trans-hom assoc (trans-hom eq (sym-hom assoc ) ) | |
| 212 | |
| 1072 | 213 iso-mono→ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b c : Obj A } {m : Hom A a b} ( mono : Mono A m ) (i : Iso A c a ) → Mono A (A [ m o Iso.≅→ i ] ) |
| 214 iso-mono→ A {a} {b} {c} {m} mono i = record { isMono = λ {d} f g → im f g } where | |
| 215 im : {d : Obj A} (f g : Hom A d c ) → A [ A [ A [ m o Iso.≅→ i ] o f ] ≈ A [ A [ m o Iso.≅→ i ] o g ] ] → A [ f ≈ g ] | |
| 216 im {d} f g mf=mg = begin | |
| 217 f ≈↑⟨ idL ⟩ | |
| 218 id1 A _ o f ≈↑⟨ car (Iso.iso→ i) ⟩ | |
| 219 ( Iso.≅← i o Iso.≅→ i) o f ≈↑⟨ assoc ⟩ | |
| 220 Iso.≅← i o (Iso.≅→ i o f) ≈⟨ cdr ( Mono.isMono mono _ _ (if=ig mf=mg) ) ⟩ | |
| 221 Iso.≅← i o (Iso.≅→ i o g) ≈⟨ assoc ⟩ | |
| 222 ( Iso.≅← i o Iso.≅→ i) o g ≈⟨ car (Iso.iso→ i) ⟩ | |
| 223 id1 A _ o g ≈⟨ idL ⟩ | |
| 224 g ∎ where | |
| 225 open ≈-Reasoning A | |
| 226 if=ig : ( m o Iso.≅→ i ) o f ≈ ( m o Iso.≅→ i ) o g → m o (Iso.≅→ i o f ) ≈ m o ( Iso.≅→ i o g ) | |
| 227 if=ig eq = trans-hom assoc (trans-hom eq (sym-hom assoc ) ) | |
| 1069 | 228 |
| 1074 | 229 ---- |
| 230 -- | |
| 231 -- Sub Object Classifier as Topos | |
| 232 -- pull back on | |
| 233 -- | |
| 1097 | 234 -- m ∙ f ≈ m ∙ g → f ≈ g |
| 235 -- | |
| 1074 | 236 -- iso ○ b |
| 1097 | 237 -- e ⇐====⇒ b -----------→ 1 |
| 1074 | 238 -- | | | |
| 239 -- | m | | ⊤ | |
| 1097 | 240 -- | ↓ char m ↓ |
| 241 -- + ------→ a -----------→ Ω | |
| 1074 | 242 -- ker h h |
| 243 -- | |
| 1097 | 244 -- Ker h = Equalizer (char m mono) (⊤ ∙ ○ a ) |
| 245 -- m = Equalizer (char m mono) (⊤ ∙ ○ a ) | |
| 246 -- | |
| 1074 | 247 -- if m is an equalizer, there is an iso between e and b as k, and if we have the iso, m becomes an equalizer. |
| 248 -- equalizer.equalizerIso : {a b c : Obj A} → (f g : Hom A a b ) → (equ : Equalizer A f g ) | |
| 249 -- → (m : Hom A c a) → ( ker-iso : IsoL A m (equalizer equ) ) → IsEqualizer A m f g | |
| 250 | |
| 975 | 251 record IsTopos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) |
| 952 | 252 ( Ω : Obj A ) |
| 975 | 253 ( ⊤ : Hom A (CCC.１ c) Ω ) |
| 254 (Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (CCC.○ c a) ])) | |
| 952 | 255 (char : {a b : Obj A} → (m : Hom A b a) → Mono A m → Hom A a Ω) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where |
| 950 | 256 field |
| 1071 | 257 ker-m : {a b : Obj A} → (m : Hom A b a ) → (mono : Mono A m) → IsEqualizer A m (char m mono) (A [ ⊤ o (CCC.○ c a) ]) |
| 1075 | 258 char-uniqueness : {a b : Obj A } {h : Hom A a Ω} |
| 259 → A [ char (equalizer (Ker h)) (record { isMono = λ f g → monic (Ker h)}) ≈ h ] | |
| 260 char-iso : {a a' b : Obj A} → (p : Hom A a b ) (q : Hom A a' b ) → (mp : Mono A p) →(mq : Mono A q) → | |
|
1095
0211d99f29fc
Topos Sets char-iso done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1075
diff
changeset
|
261 (i : Iso A a a' ) → A [ p ≈ A [ q o Iso.≅→ i ] ] → A [ char p mp ≈ char q mq ] |
| 1097 | 262 -- this means, char m is unique among all equalizers of h and ○ a |
| 1075 | 263 char-cong : {a b : Obj A } { m m' : Hom A b a } { mono : Mono A m } { mono' : Mono A m' } |
| 1070 | 264 → A [ m ≈ m' ] → A [ char m mono ≈ char m' mono' ] |
|
1095
0211d99f29fc
Topos Sets char-iso done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1075
diff
changeset
|
265 char-cong {a} {b} {m} {m'} {mo} {mo'} m=m' = char-iso m m' mo mo' (≡-iso A _) ( begin |
|
0211d99f29fc
Topos Sets char-iso done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1075
diff
changeset
|
266 m ≈⟨ m=m' ⟩ |
|
0211d99f29fc
Topos Sets char-iso done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1075
diff
changeset
|
267 m' ≈↑⟨ idR ⟩ |
|
0211d99f29fc
Topos Sets char-iso done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
1075
diff
changeset
|
268 m' o Iso.≅→ (≡-iso A b) ∎ ) where open ≈-Reasoning A |
| 1016 | 269 ker : {a : Obj A} → ( h : Hom A a Ω ) → Hom A ( equalizer-c (Ker h) ) a |
| 270 ker h = equalizer (Ker h) | |
| 271 char-m=⊤ : {a b : Obj A} → (m : Hom A b a) → (mono : Mono A m) → A [ A [ char m mono o m ] ≈ A [ ⊤ o CCC.○ c b ] ] | |
| 272 char-m=⊤ {a} {b} m mono = begin | |
| 1018 | 273 char m mono o m ≈⟨ IsEqualizer.fe=ge (ker-m m mono) ⟩ |
| 1016 | 274 (⊤ o CCC.○ c a) o m ≈↑⟨ assoc ⟩ |
| 275 ⊤ o (CCC.○ c a o m ) ≈⟨ cdr (IsCCC.e2 (CCC.isCCC c)) ⟩ | |
| 276 ⊤ o CCC.○ c b ∎ where open ≈-Reasoning A | |
| 950 | 277 |
| 975 | 278 record Topos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where |
| 952 | 279 field |
| 950 | 280 Ω : Obj A |
| 975 | 281 ⊤ : Hom A (CCC.１ c) Ω |
| 282 Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (CCC.○ c a) ]) | |
| 952 | 283 char : {a b : Obj A} → (m : Hom A b a ) → Mono A m → Hom A a Ω |
| 975 | 284 isTopos : IsTopos A c Ω ⊤ Ker char |
| 973 | 285 Monik : {a : Obj A} (h : Hom A a Ω) → Mono A (equalizer (Ker h)) |
| 286 Monik h = record { isMono = λ f g → monic (Ker h ) } | |
| 783 | 287 |
| 963 | 288 record NatD {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where |
| 289 field | |
| 290 Nat : Obj A | |
| 291 nzero : Hom A １ Nat | |
| 292 nsuc : Hom A Nat Nat | |
| 293 | |
| 294 open NatD | |
| 295 | |
| 986 | 296 record IsToposNat {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) (iNat : NatD A １ ) |
| 297 ( initialNat : (nat : NatD A １ ) → Hom A (Nat iNat) (Nat nat) ) | |
| 963 | 298 : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where |
| 299 field | |
| 986 | 300 izero : (nat : NatD A １ ) → A [ A [ initialNat nat o nzero iNat ] ≈ nzero nat ] |
| 301 isuc : (nat : NatD A １ ) → A [ A [ initialNat nat o nsuc iNat ] ≈ A [ nsuc nat o initialNat nat ] ] | |
| 963 | 302 |
| 303 record ToposNat {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where | |
| 304 field | |
| 986 | 305 iNat : NatD A １ |
| 306 initialNat : (nat : NatD A １ ) → Hom A (Nat iNat) (Nat nat) | |
| 307 nat-unique : (nat : NatD A １ ) → {g : Hom A (Nat iNat) (Nat nat) } | |
| 308 → A [ A [ g o nzero iNat ] ≈ nzero nat ] | |
| 309 → A [ A [ g o nsuc iNat ] ≈ A [ nsuc nat o g ] ] | |
| 310 → A [ g ≈ initialNat nat ] | |
| 311 isToposN : IsToposNat A １ iNat initialNat | |
| 783 | 312 |