1 Generalizable All Variables.
2 Require Import Preamble.
3 Require Import General.
4 Require Import Categories_ch1_3.
5 Require Import Functors_ch1_4.
6 Require Import Isomorphisms_ch1_5.
7 Require Import ProductCategories_ch1_6_1.
8 Require Import InitialTerminal_ch2_2.
9 Require Import Subcategories_ch7_1.
10 Require Import NaturalTransformations_ch7_4.
11 Require Import NaturalIsomorphisms_ch7_5.
12 Require Import Coherence_ch7_8.
13 Require Import BinoidalCategories.
14 Require Import PreMonoidalCategories.
15 Require Import MonoidalCategories_ch7_8.
17 (******************************************************************************)
18 (* Chapter 2.8: Hom Sets and Enriched Categories *)
19 (******************************************************************************)
21 Class ECategory `(mn:PreMonoidalCat(bc:=bc)(C:=V)(I:=EI))(Eob:Type)(Ehom:Eob->Eob->V) :=
22 { ehom := Ehom where "a ~~> b" := (ehom a b)
25 ; eid : forall a, EI~>(a~~>a)
26 ; eid_central : forall a, CentralMorphism (eid a)
27 ; ecomp : forall {a b c}, (a~~>b)⊗(b~~>c) ~> (a~~>c)
28 ; ecomp_central :> forall {a b c}, CentralMorphism (@ecomp a b c)
29 ; eleft_identity : forall {a b }, eid a ⋉ (a~~>b) >>> ecomp ~~ #(pmon_cancell _ _)
30 ; eright_identity : forall {a b }, (a~~>b) ⋊ eid b >>> ecomp ~~ #(pmon_cancelr _ _)
31 ; eassociativity : forall {a b c d}, #(pmon_assoc _ _ _ (_~~>_))⁻¹ >>> ecomp ⋉ (c~~>d) >>> ecomp ~~ (a~~>b) ⋊ ecomp >>> ecomp
33 Notation "a ~~> b" := (@ehom _ _ _ _ _ _ _ _ _ _ a b) : category_scope.
34 Coercion eob_eob : ECategory >-> Sortclass.
36 Lemma ecomp_is_functorial `{ec:ECategory}{a b c}{x}(f:EI~~{V}~~>(a~~>b))(g:EI~~{V}~~>(b~~>c)) :
37 ((x ~~> a) ⋊-) \ (iso_backward ((pmon_cancelr mn) EI) >>> ((- ⋉EI) \ f >>> (((a ~~> b) ⋊-) \ g >>> ecomp))) >>> ecomp ~~
38 ((x ~~> a) ⋊-) \ f >>> (ecomp >>> (#((pmon_cancelr mn) (x ~~> b)) ⁻¹ >>> (((x ~~> b) ⋊-) \ g >>> ecomp))).
40 set (@fmor_preserves_comp) as fmor_preserves_comp'.
42 (* knock off the leading (x ~~> a) ⋊ f *)
43 repeat setoid_rewrite <- associativity.
44 set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) f) as qq.
45 apply iso_shift_right' in qq.
46 setoid_rewrite <- associativity in qq.
48 apply iso_shift_left' in qq.
53 repeat setoid_rewrite associativity.
54 repeat setoid_rewrite <- fmor_preserves_comp'.
55 repeat setoid_rewrite associativity.
56 apply comp_respects; try reflexivity.
58 (* rewrite using the lemma *)
59 assert (forall {a b c x}(g:EI~~{V}~~>(b ~~> c)),
60 ((bin_second(BinoidalCat:=bc) (x ~~> a)) \ ((bin_second(BinoidalCat:=bc) (a ~~> b)) \ g))
62 (#(pmon_assoc mn (x ~~> a) _ _)⁻¹ >>>
63 (bin_second(BinoidalCat:=bc) ((x ~~> a) ⊗ (a ~~> b))) \ g >>> #(pmon_assoc mn (x ~~> a) _ _))).
66 setoid_rewrite associativity.
68 apply iso_shift_right'.
69 setoid_rewrite <- pmon_coherent_l.
70 set (ni_commutes (pmon_assoc_ll (x0~~>a0) (a0~~>b0))) as qq.
76 (* rewrite using eassociativity *)
77 repeat setoid_rewrite associativity.
78 set (@eassociativity _ _ _ _ _ _ _ _ _ ec x a) as qq.
83 (* knock off the trailing ecomp *)
84 repeat setoid_rewrite <- associativity.
85 apply comp_respects; try reflexivity.
87 (* cancel out the adjacent assoc/cossa pair *)
88 repeat setoid_rewrite associativity.
89 setoid_rewrite juggle2.
91 apply comp_respects; [ idtac |
92 repeat setoid_rewrite <- associativity;
93 etransitivity; [ idtac | apply left_identity ];
94 apply comp_respects; [ idtac | reflexivity ];
98 (* now swap the order of ecomp⋉(b ~~> c) and ((x ~~> a) ⊗ (a ~~> b))⋊g *)
99 repeat setoid_rewrite associativity.
100 set (@centralmor_first) as se.
101 setoid_rewrite <- se.
104 (* and knock the trailing (x ~~> b)⋊ g off *)
105 repeat setoid_rewrite <- associativity.
106 apply comp_respects; try reflexivity.
108 (* push the ecomp forward past the rlecnac *)
109 set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) (@ecomp _ _ _ _ _ _ _ _ _ ec x a b)) as qq.
111 apply iso_shift_left' in qq.
112 setoid_rewrite associativity in qq.
114 apply iso_shift_right' in qq.
119 (* and knock off the trailing ecomp *)
120 apply comp_respects; try reflexivity.
122 setoid_replace (iso_backward ((pmon_cancelr mn) ((x ~~> a) ⊗ (a ~~> b)))) with
123 (iso_backward ((pmon_cancelr mn) ((x ~~> a) ⊗ (a ~~> b))) >>> id _).
125 set (@iso_shift_right') as ibs.
130 setoid_rewrite (MacLane_ex_VII_1_1 (x~~>a) (a~~>b)).
131 setoid_rewrite juggle3.
132 set (fmor_preserves_comp ((x ~~> a) ⋊-)) as q.
136 setoid_rewrite iso_comp1.
137 setoid_rewrite fmor_preserves_id.
138 setoid_rewrite right_identity.
143 apply right_identity.
147 Lemma underlying_associativity `{ec:ECategory(mn:=mn)(EI:=EI)(Eob:=Eob)(Ehom:=Ehom)} :
148 forall {a b : Eob} (f : EI ~~{ V }~~> a ~~> b) {c : Eob}
149 (g : EI ~~{ V }~~> b ~~> c) {d : Eob} (h : EI ~~{ V }~~> c ~~> d),
150 ((((#((pmon_cancelr mn) EI) ⁻¹ >>> (f ⋉ EI >>> (a ~~> b) ⋊ g)) >>> ecomp) ⋉ EI >>> (a ~~> c) ⋊ h)) >>> ecomp ~~
151 ((f ⋉ EI >>> (a ~~> b) ⋊ ((#((pmon_cancelr mn) EI) ⁻¹ >>> (g ⋉ EI >>> (b ~~> c) ⋊ h)) >>> ecomp))) >>> ecomp.
153 intros; symmetry; etransitivity;
154 [ setoid_rewrite associativity; apply comp_respects;
155 [ apply reflexivity | repeat setoid_rewrite associativity; apply (ecomp_is_functorial(x:=a) g h) ] | idtac ].
157 repeat setoid_rewrite <- fmor_preserves_comp.
158 repeat setoid_rewrite <- associativity.
159 apply comp_respects; try reflexivity.
160 apply comp_respects; try reflexivity.
162 set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) f) as qq.
163 apply iso_shift_right' in qq.
165 setoid_rewrite <- associativity in qq.
166 apply iso_shift_left' in qq.
167 apply (fmor_respects (bin_first EI)) in qq.
168 setoid_rewrite <- fmor_preserves_comp in qq.
172 repeat setoid_rewrite <- fmor_preserves_comp.
173 repeat setoid_rewrite associativity.
174 apply comp_respects; try reflexivity.
176 repeat setoid_rewrite associativity.
177 set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) (@ecomp _ _ _ _ _ _ _ _ _ ec a b c)) as qq.
178 apply iso_shift_right' in qq.
180 setoid_rewrite <- associativity in qq.
181 apply iso_shift_left' in qq.
187 repeat setoid_rewrite <- associativity.
188 apply comp_respects; try reflexivity.
192 (iso_backward ((pmon_cancelr mn) (a ~~> b)) ⋉ EI >>> ((a ~~> b) ⋊ g) ⋉ EI) ((a ~~> b) ⋊ g)
193 (((pmon_cancelr mn) ((a ~~> b) ⊗ (b ~~> c))))) as xx.
195 etransitivity; [ apply xx | apply comp_respects; try reflexivity ].
198 setoid_rewrite (fmor_preserves_comp (bin_first EI)).
199 set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) ((iso_backward ((pmon_cancelr mn) (a ~~> b)) >>> (a ~~> b) ⋊ g))) as qq.
201 setoid_rewrite <- qq.
204 setoid_rewrite <- associativity.
205 setoid_rewrite iso_comp1.
210 Instance Underlying `(ec:ECategory(mn:=mn)(EI:=EI)(Eob:=Eob)(Ehom:=Ehom)) : Category Eob (fun a b => EI~>(a~~>b)) :=
211 { id := fun a => eid a
212 ; comp := fun a b c g f => #(pmon_cancelr _ _)⁻¹ >>> (g ⋉ _ >>> _ ⋊ f) >>> ecomp
213 ; eqv := fun a b (f:EI~>(a~~>b))(g:EI~>(a~~>b)) => f ~~ g
215 abstract (intros; apply Build_Equivalence;
218 | unfold Transitive]; intros; simpl; auto).
219 abstract (intros; unfold Proper; unfold respectful; intros; simpl;
220 repeat apply comp_respects; try apply reflexivity;
221 [ apply (fmor_respects (bin_first EI)) | idtac ]; auto;
222 apply (fmor_respects (bin_second (a~~>b))); auto).
224 set (fun c d => centralmor_first(c:=c)(d:=d)(CentralMorphism:=(eid_central a))) as q;
226 repeat setoid_rewrite associativity;
227 setoid_rewrite eleft_identity;
228 setoid_rewrite <- (ni_commutes (@pmon_cancell _ _ _ _ _ _ mn));
229 setoid_rewrite <- associativity;
230 set (coincide pmon_triangle) as qq;
233 setoid_rewrite iso_comp2;
234 apply left_identity).
236 repeat setoid_rewrite associativity;
237 setoid_rewrite eright_identity;
238 setoid_rewrite <- (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn));
239 setoid_rewrite <- associativity;
241 setoid_rewrite iso_comp2;
242 apply left_identity).
244 repeat setoid_rewrite associativity;
245 apply comp_respects; try reflexivity;
246 repeat setoid_rewrite <- associativity;
247 apply underlying_associativity).
249 Coercion Underlying : ECategory >-> Category.
252 `{mn:PreMonoidalCat(bc:=bc)(C:=V)(I:=EI)}
253 {Eob1}{EHom1}(ec1:ECategory mn Eob1 EHom1)
254 {Eob2}{EHom2}(ec2:ECategory mn Eob2 EHom2)
255 (EFobj : Eob1 -> Eob2)
257 { efunc_fobj := EFobj
258 ; efunc : forall a b:Eob1, (a ~~> b) ~~{V}~~> ( (EFobj a) ~~> (EFobj b) )
259 ; efunc_central : forall a b, CentralMorphism (efunc a b)
260 ; efunc_preserves_id : forall a, eid a >>> efunc a a ~~ eid (EFobj a)
261 ; efunc_preserves_comp : forall a b c, (efunc a b) ⋉ _ >>> _ ⋊ (efunc b c) >>> ecomp ~~ ecomp >>> efunc a c
263 Coercion efunc_fobj : EFunctor >-> Funclass.
264 Implicit Arguments efunc [ Ob Hom V bin_obj' bc EI mn Eob1 EHom1 ec1 Eob2 EHom2 ec2 EFobj ].
266 Definition efunctor_id
267 `{mn:PreMonoidalCat(bc:=bc)(C:=V)(I:=EI)}
268 {Eob1}{EHom1}(ec1:ECategory mn Eob1 EHom1)
269 : EFunctor ec1 ec1 (fun x => x).
270 refine {| efunc := fun a b => id (a ~~> b) |}.
271 abstract (intros; apply Build_CentralMorphism; intros;
272 setoid_rewrite fmor_preserves_id;
273 setoid_rewrite right_identity;
274 setoid_rewrite left_identity;
276 abstract (intros; apply right_identity).
278 setoid_rewrite fmor_preserves_id;
279 setoid_rewrite right_identity;
280 setoid_rewrite left_identity;
284 Definition efunctor_comp
285 `{mn:PreMonoidalCat(bc:=bc)(C:=V)(I:=EI)}
286 {Eob1}{EHom1}(ec1:ECategory mn Eob1 EHom1)
287 {Eob2}{EHom2}(ec2:ECategory mn Eob2 EHom2)
288 {Eob3}{EHom3}(ec3:ECategory mn Eob3 EHom3)
289 {Fobj}(F:EFunctor ec1 ec2 Fobj)
290 {Gobj}(G:EFunctor ec2 ec3 Gobj)
291 : EFunctor ec1 ec3 (Gobj ○ Fobj).
292 refine {| efunc := fun a b => (efunc F a b) >>> (efunc G _ _) |}; intros; simpl.
293 abstract (apply Build_CentralMorphism; intros;
294 [ set (fun a b c d => centralmor_first(CentralMorphism:=(efunc_central(EFunctor:=F)) a b)(c:=c)(d:=d)) as fc1
295 ; set (fun a b c d => centralmor_first(CentralMorphism:=(efunc_central(EFunctor:=G)) a b)(c:=c)(d:=d)) as gc1
296 ; setoid_rewrite <- (fmor_preserves_comp (-⋉d))
297 ; setoid_rewrite <- (fmor_preserves_comp (-⋉c))
298 ; setoid_rewrite <- associativity
299 ; setoid_rewrite <- fc1
300 ; setoid_rewrite associativity
301 ; setoid_rewrite <- gc1
303 | set (fun a b c d => centralmor_second(CentralMorphism:=(efunc_central(EFunctor:=F)) a b)(c:=c)(d:=d)) as fc2
304 ; set (fun a b c d => centralmor_second(CentralMorphism:=(efunc_central(EFunctor:=G)) a b)(c:=c)(d:=d)) as gc2
305 ; setoid_rewrite <- (fmor_preserves_comp (d⋊-))
306 ; setoid_rewrite <- (fmor_preserves_comp (c⋊-))
307 ; setoid_rewrite <- associativity
309 ; setoid_rewrite associativity
312 abstract (setoid_rewrite <- associativity;
313 setoid_rewrite efunc_preserves_id;
314 setoid_rewrite efunc_preserves_id;
316 abstract (repeat setoid_rewrite associativity;
317 set (fmor_preserves_comp (-⋉(b~~>c))) as q; setoid_rewrite <- q; clear q;
318 repeat setoid_rewrite associativity;
319 set (fmor_preserves_comp (((Gobj (Fobj a) ~~> Gobj (Fobj b))⋊-))) as q; setoid_rewrite <- q; clear q;
320 set (fun d e => centralmor_second(c:=d)(d:=e)(CentralMorphism:=(efunc_central(EFunctor:=F) b c))) as qq;
321 setoid_rewrite juggle2;
322 setoid_rewrite juggle2;
325 repeat setoid_rewrite associativity;
326 set ((efunc_preserves_comp(EFunctor:=G)) (Fobj a) (Fobj b) (Fobj c)) as q;
327 repeat setoid_rewrite associativity;
328 repeat setoid_rewrite associativity in q;
331 repeat setoid_rewrite <- associativity;
332 apply comp_respects; try reflexivity;
333 set ((efunc_preserves_comp(EFunctor:=F)) a b c) as q;
337 Instance UnderlyingFunctor `(EF:@EFunctor Ob Hom V bin_obj' bc EI mn Eob1 EHom1 ec1 Eob2 EHom2 ec2 Eobj)
338 : Functor (Underlying ec1) (Underlying ec2) Eobj :=
339 { fmor := fun a b (f:EI~~{V}~~>(a~~>b)) => f >>> (efunc _ a b) }.
340 abstract (intros; simpl; apply comp_respects; try reflexivity; auto).
341 abstract (intros; simpl; apply efunc_preserves_id).
344 repeat setoid_rewrite associativity;
345 setoid_rewrite <- efunc_preserves_comp;
346 repeat setoid_rewrite associativity;
347 apply comp_respects; try reflexivity;
348 set (@fmor_preserves_comp _ _ _ _ _ _ _ (bin_first EI)) as qq;
349 setoid_rewrite <- qq;
351 repeat setoid_rewrite associativity;
352 apply comp_respects; try reflexivity;
353 repeat setoid_rewrite <- associativity;
354 apply comp_respects; try reflexivity;
355 set (@fmor_preserves_comp _ _ _ _ _ _ _ (bin_second (Eobj a ~~> Eobj b))) as qq;
356 setoid_rewrite <- qq;
357 repeat setoid_rewrite <- associativity;
358 apply comp_respects; try reflexivity;
360 apply (centralmor_first(CentralMorphism:=(efunc_central a b)))).
362 Coercion UnderlyingFunctor : EFunctor >-> Functor.
364 Structure Enrichment :=
366 ; enr_v_hom : enr_v_ob -> enr_v_ob -> Type
367 ; enr_v : Category enr_v_ob enr_v_hom
368 ; enr_v_fobj : prod_obj enr_v enr_v -> enr_v_ob
369 ; enr_v_f : Functor (enr_v ×× enr_v) enr_v enr_v_fobj
371 ; enr_v_mon : MonoidalCat enr_v enr_v_fobj enr_v_f enr_v_i
373 ; enr_c_hom : enr_c_obj -> enr_c_obj -> enr_v
374 ; enr_c : ECategory enr_v_mon enr_c_obj enr_c_hom
376 Coercion enr_c : Enrichment >-> ECategory.
378 (* an enrichment for which every object of the enriching category is the tensor of finitely many hom-objects *)
379 Structure SurjectiveEnrichment (e:Enrichment) :=
381 ; se_decomp : @treeDecomposition (enr_v e) (option ((enr_c_obj e)*(enr_c_obj e)))
382 (fun t => match t with
384 | Some x => match x with pair y z => enr_c_hom e y z end
386 (fun d1 d2:enr_v e => enr_v_fobj e (pair_obj d1 d2))
388 Coercion se_enr : SurjectiveEnrichment >-> Enrichment.
390 (* Enriched Fibrations *)
393 Context `{E:ECategory}.
394 Context {Eob2}{Ehom2}{B:@ECategory Ob Hom V bin_obj' mn EI mn Eob2 Ehom2}.
395 Context {efobj}(F:EFunctor E B efobj).
398 * A morphism is prone if its image factors through the image of
399 * another morphism with the same codomain just in case the factor
400 * is the image of a unique morphism. One might say that it
401 * "uniquely reflects factoring through morphisms with the same
404 Definition Prone {e e'}(φ:EI~~{V}~~>(e'~~>e)) :=
405 forall e'' (ψ:EI~~{V}~~>(e''~~>e)) (g:(efobj e'')~~{B}~~>(efobj e')),
406 (comp(Category:=B) _ _ _ g (φ >>> (efunc F _ _))) ~~
408 -> { χ:e''~~{E}~~>e' & ψ ~~ χ >>> φ & g ~~ comp(Category:=V) _ _ _ χ (efunc F e'' e') }.
409 (* FIXME: χ must also be unique *)
411 (* a functor is a Street Fibration if morphisms with codomain in its image are, up to iso, the images of prone morphisms *)
413 (* Street was the first to define non-evil fibrations using isomorphisms (for cleavage_pf below) rather than equality *)
414 Structure StreetCleavage (e:E)(b:B)(f:b~~{B}~~>(efobj e)) :=
416 ; cleavage_pf : (efobj cleavage_e') ≅ b
417 ; cleavage_phi : cleavage_e' ~~{E}~~> e
418 ; cleavage_cart : Prone cleavage_phi
419 ; cleavage_eqv : #cleavage_pf >>> f ~~ comp(Category:=V) _ _ _ cleavage_phi (efunc F _ _)
422 (* if V, the category enriching E and B is V-enriched, we get a functor Bop->Vint *)
424 (* Every equivalence of categories is a Street fibration *)
426 (* this is actually a "Street Fibration", the non-evil version of a Grothendieck Fibration *)
427 Definition EFibration := forall e b f, exists cl:StreetCleavage e b f, True.
429 Definition ClovenEFibration := forall e b f, StreetCleavage e b f.
432 * Now, a language has polymorphic types iff its category of
433 * judgments contains a second enriched category, the category of
434 * Kinds, and the category of types is fibered over the category of
435 * Kinds, and the weakening functor-of-fibers has a right adjoint.
437 * http://ncatlab.org/nlab/show/Grothendieck+fibration
439 * I suppose we'll need to also ask that the R-functors takes
440 * Prone morphisms to Prone morphisms.