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