|
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
|
|
950
|
184 open Equalizer
|
|
963
|
185 open import equalizer
|
|
950
|
186
|
|
952
|
187 record Mono {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {b a : Obj A} (mono : Hom A b a) : Set (c₁ ⊔ c₂ ⊔ ℓ) where
|
|
|
188 field
|
|
|
189 isMono : {c : Obj A} ( f g : Hom A c b ) → A [ A [ mono o f ] ≈ A [ mono o g ] ] → A [ f ≈ g ]
|
|
|
190
|
|
|
191 open Mono
|
|
|
192
|
|
1069
|
193 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 ] )
|
|
|
194 iso-mono A {a} {b} {c} {m} mono i = record { isMono = λ {d} f g → im f g } where
|
|
|
195 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 ]
|
|
|
196 im {d} f g mf=mg = begin
|
|
|
197 f ≈↑⟨ idL ⟩
|
|
|
198 id1 A _ o f ≈↑⟨ car (Iso.iso← i) ⟩
|
|
|
199 ( Iso.≅→ i o Iso.≅← i) o f ≈↑⟨ assoc ⟩
|
|
|
200 Iso.≅→ i o (Iso.≅← i o f) ≈⟨ cdr ( Mono.isMono mono _ _ (if=ig mf=mg) ) ⟩
|
|
|
201 Iso.≅→ i o (Iso.≅← i o g) ≈⟨ assoc ⟩
|
|
|
202 ( Iso.≅→ i o Iso.≅← i) o g ≈⟨ car (Iso.iso← i) ⟩
|
|
|
203 id1 A _ o g ≈⟨ idL ⟩
|
|
|
204 g ∎ where
|
|
|
205 open ≈-Reasoning A
|
|
|
206 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 )
|
|
|
207 if=ig eq = trans-hom assoc (trans-hom eq (sym-hom assoc ) )
|
|
|
208
|
|
1072
|
209 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 ] )
|
|
|
210 iso-mono→ A {a} {b} {c} {m} mono i = record { isMono = λ {d} f g → im f g } where
|
|
|
211 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 ]
|
|
|
212 im {d} f g mf=mg = begin
|
|
|
213 f ≈↑⟨ idL ⟩
|
|
|
214 id1 A _ o f ≈↑⟨ car (Iso.iso→ i) ⟩
|
|
|
215 ( Iso.≅← i o Iso.≅→ i) o f ≈↑⟨ assoc ⟩
|
|
|
216 Iso.≅← i o (Iso.≅→ i o f) ≈⟨ cdr ( Mono.isMono mono _ _ (if=ig mf=mg) ) ⟩
|
|
|
217 Iso.≅← i o (Iso.≅→ i o g) ≈⟨ assoc ⟩
|
|
|
218 ( Iso.≅← i o Iso.≅→ i) o g ≈⟨ car (Iso.iso→ i) ⟩
|
|
|
219 id1 A _ o g ≈⟨ idL ⟩
|
|
|
220 g ∎ where
|
|
|
221 open ≈-Reasoning A
|
|
|
222 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 )
|
|
|
223 if=ig eq = trans-hom assoc (trans-hom eq (sym-hom assoc ) )
|
|
1069
|
224
|
|
1074
|
225 ----
|
|
|
226 --
|
|
|
227 -- Sub Object Classifier as Topos
|
|
|
228 -- pull back on
|
|
|
229 --
|
|
|
230 -- iso ○ b
|
|
|
231 -- e ⇐====⇒ b -----------→ 1 m ∙ f ≈ m ∙ g → f ≈ g
|
|
|
232 -- | | |
|
|
|
233 -- | m | | ⊤
|
|
|
234 -- | ↓ char m ↓ Ker h = Equalizer (char m mono) (⊤ ∙ ○ a )
|
|
|
235 -- + ------→ a -----------→ Ω m = Equalizer (char m mono) (⊤ ∙ ○ a )
|
|
|
236 -- ker h h
|
|
|
237 --
|
|
|
238 -- 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.
|
|
|
239 -- equalizer.equalizerIso : {a b c : Obj A} → (f g : Hom A a b ) → (equ : Equalizer A f g )
|
|
|
240 -- → (m : Hom A c a) → ( ker-iso : IsoL A m (equalizer equ) ) → IsEqualizer A m f g
|
|
|
241
|
|
975
|
242 record IsTopos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A)
|
|
952
|
243 ( Ω : Obj A )
|
|
975
|
244 ( ⊤ : Hom A (CCC.１ c) Ω )
|
|
|
245 (Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (CCC.○ c a) ]))
|
|
952
|
246 (char : {a b : Obj A} → (m : Hom A b a) → Mono A m → Hom A a Ω) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where
|
|
950
|
247 field
|
|
1071
|
248 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) ])
|
|
1072
|
249 char-iso : {a b : Obj A } {m : Hom A a b} {h : Hom A b Ω}( mono : Mono A m ) → ( i : Iso A a (equalizer-c (Ker h)) )
|
|
1069
|
250 → A [ char (A [ m o Iso.≅← i ]) (iso-mono A mono i) ≈ h ]
|
|
1071
|
251 char-cong : {a b : Obj A } { m m' : Hom A b a } { mono : Mono A m } { mono' : Mono A m' }
|
|
1070
|
252 → A [ m ≈ m' ] → A [ char m mono ≈ char m' mono' ]
|
|
1016
|
253 ker : {a : Obj A} → ( h : Hom A a Ω ) → Hom A ( equalizer-c (Ker h) ) a
|
|
|
254 ker h = equalizer (Ker h)
|
|
1071
|
255 char-uniqueness : {a b : Obj A } {h : Hom A a Ω}
|
|
|
256 → A [ char (equalizer (Ker h)) (record { isMono = λ f g → monic (Ker h)}) ≈ h ]
|
|
|
257 char-uniqueness {a} {b} {h} = begin
|
|
1072
|
258 char (equalizer (Ker h)) (record { isMono = λ f g → monic (Ker h)}) ≈⟨ char-cong (
|
|
|
259 begin
|
|
|
260 equalizer (Ker h) ≈↑⟨ idR ⟩
|
|
|
261 equalizer (Ker h) o id1 A _ ≈↑⟨ cdr (idR) ⟩
|
|
|
262 equalizer (Ker h) o ( id1 A _ o id1 A _ ) ≈⟨ assoc ⟩
|
|
|
263 (equalizer (Ker h) o Iso.≅→ (≡-iso A _)) o Iso.≅← (≡-iso A _) ∎ ) ⟩
|
|
|
264 char ( ( equalizer (Ker h) o Iso.≅→ (≡-iso A _)) o Iso.≅← (≡-iso A _) ) (iso-mono A (≡-mono→ h) (≡-iso A _)) ≈⟨ char-iso (≡-mono→ h) (≡-iso A _) ⟩
|
|
1071
|
265 h ∎ where
|
|
|
266 open ≈-Reasoning A
|
|
1072
|
267 ≡-mono→ : {a : Obj A } (h : Hom A a Ω) →
|
|
1071
|
268 Mono A ( equalizer (Ker h) o (Iso.≅→ (≡-iso A (equalizer-c (Ker h)))))
|
|
1072
|
269 ≡-mono→ {a} h = iso-mono→ A (record { isMono = λ f g → monic (Ker h)} ) (≡-iso A _)
|
|
1016
|
270 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 ] ]
|
|
|
271 char-m=⊤ {a} {b} m mono = begin
|
|
1018
|
272 char m mono o m ≈⟨ IsEqualizer.fe=ge (ker-m m mono) ⟩
|
|
1016
|
273 (⊤ o CCC.○ c a) o m ≈↑⟨ assoc ⟩
|
|
|
274 ⊤ o (CCC.○ c a o m ) ≈⟨ cdr (IsCCC.e2 (CCC.isCCC c)) ⟩
|
|
|
275 ⊤ o CCC.○ c b ∎ where open ≈-Reasoning A
|
|
950
|
276
|
|
975
|
277 record Topos {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where
|
|
952
|
278 field
|
|
950
|
279 Ω : Obj A
|
|
975
|
280 ⊤ : Hom A (CCC.１ c) Ω
|
|
|
281 Ker : {a : Obj A} → ( h : Hom A a Ω ) → Equalizer A h (A [ ⊤ o (CCC.○ c a) ])
|
|
952
|
282 char : {a b : Obj A} → (m : Hom A b a ) → Mono A m → Hom A a Ω
|
|
975
|
283 isTopos : IsTopos A c Ω ⊤ Ker char
|
|
973
|
284 Monik : {a : Obj A} (h : Hom A a Ω) → Mono A (equalizer (Ker h))
|
|
|
285 Monik h = record { isMono = λ f g → monic (Ker h ) }
|
|
783
|
286
|
|
963
|
287 record NatD {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where
|
|
|
288 field
|
|
|
289 Nat : Obj A
|
|
|
290 nzero : Hom A １ Nat
|
|
|
291 nsuc : Hom A Nat Nat
|
|
|
292
|
|
|
293 open NatD
|
|
|
294
|
|
986
|
295 record IsToposNat {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) (iNat : NatD A １ )
|
|
|
296 ( initialNat : (nat : NatD A １ ) → Hom A (Nat iNat) (Nat nat) )
|
|
963
|
297 : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where
|
|
|
298 field
|
|
986
|
299 izero : (nat : NatD A １ ) → A [ A [ initialNat nat o nzero iNat ] ≈ nzero nat ]
|
|
|
300 isuc : (nat : NatD A １ ) → A [ A [ initialNat nat o nsuc iNat ] ≈ A [ nsuc nat o initialNat nat ] ]
|
|
963
|
301
|
|
|
302 record ToposNat {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( １ : Obj A) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where
|
|
|
303 field
|
|
986
|
304 iNat : NatD A １
|
|
|
305 initialNat : (nat : NatD A １ ) → Hom A (Nat iNat) (Nat nat)
|
|
|
306 nat-unique : (nat : NatD A １ ) → {g : Hom A (Nat iNat) (Nat nat) }
|
|
|
307 → A [ A [ g o nzero iNat ] ≈ nzero nat ]
|
|
|
308 → A [ A [ g o nsuc iNat ] ≈ A [ nsuc nat o g ] ]
|
|
|
309 → A [ g ≈ initialNat nat ]
|
|
|
310 isToposN : IsToposNat A １ iNat initialNat
|
|
783
|
311
|
