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 MonoidalCategories_ch7_8.
15 (******************************************************************************)
16 (* Chapter 2.8: Hom Sets and Enriched Categories                              *)
17 (******************************************************************************)
19 Class ECategory `(mn:PreMonoidalCat(bc:=bc)(C:=V)(I:=EI))(Eob:Type)(Ehom:Eob->Eob->V) :=
20 { ehom               :=  Ehom where "a ~~> b" := (ehom a b)
21 ; eob_eob            :=  Eob
22 ; e_v                :=  mn
23 ; eid                :   forall a,          EI~>(a~~>a)
24 ; eid_central        :   forall a,          CentralMorphism (eid a)
25 ; ecomp              :   forall {a b c},    (a~~>b)⊗(b~~>c) ~> (a~~>c)
26 ; ecomp_central      :>  forall {a b c},    CentralMorphism (@ecomp a b c)
27 ; eleft_identity     :   forall {a b  },    eid a ⋉ (a~~>b) >>> ecomp ~~ #(pmon_cancell _ _)
28 ; eright_identity    :   forall {a b  },    (a~~>b) ⋊ eid b >>> ecomp ~~ #(pmon_cancelr _ _)
29 ; eassociativity     :   forall {a b c d},  #(pmon_assoc _ _ _ (_~~>_))⁻¹ >>> ecomp ⋉ (c~~>d) >>> ecomp ~~ (a~~>b) ⋊ ecomp >>> ecomp
30 }.
31 Notation "a ~~> b" := (@ehom _ _ _ _ _ _ _ _ _ _ a b) : category_scope.
32 Coercion eob_eob : ECategory >-> Sortclass.
34 Lemma ecomp_is_functorial `{ec:ECategory}{a b c}{x}(f:EI~~{V}~~>(a~~>b))(g:EI~~{V}~~>(b~~>c)) :
35    ((x ~~> a) ⋊-) \ (iso_backward ((pmon_cancelr mn) EI) >>> ((- ⋉EI) \ f >>> (((a ~~> b) ⋊-) \ g >>> ecomp))) >>> ecomp ~~
36    ((x ~~> a) ⋊-) \ f >>> (ecomp >>> (#((pmon_cancelr mn) (x ~~> b)) ⁻¹ >>> (((x ~~> b) ⋊-) \ g >>> ecomp))).
38    set (@fmor_preserves_comp) as fmor_preserves_comp'.
40    (* knock off the leading (x ~~> a) ⋊ f *)
41    repeat setoid_rewrite <- associativity.
42    set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) f) as qq.
43    apply iso_shift_right' in qq.
44    setoid_rewrite <- associativity in qq.
45    apply symmetry in qq.
46    apply iso_shift_left' in qq.
47    apply symmetry in qq.
48    simpl in qq.
49    setoid_rewrite <- qq.
50    clear qq.
51    repeat setoid_rewrite associativity.
52    repeat setoid_rewrite <- fmor_preserves_comp'.
53    repeat setoid_rewrite associativity.
54    apply comp_respects; try reflexivity.
56    (* rewrite using the lemma *)
57    assert (forall {a b c x}(g:EI~~{V}~~>(b ~~> c)),
58     ((bin_second(BinoidalCat:=bc) (x ~~> a)) \ ((bin_second(BinoidalCat:=bc) (a ~~> b)) \ g))
59     ~~
60     (#(pmon_assoc mn (x ~~> a) _ _)⁻¹ >>>
61      (bin_second(BinoidalCat:=bc) ((x ~~> a) ⊗ (a ~~> b))) \ g >>> #(pmon_assoc mn (x ~~> a) _ _))).
62     symmetry.
64     setoid_rewrite associativity.
65     symmetry.
66     apply iso_shift_right'.
67     setoid_rewrite <- pmon_coherent_l.
68     set (ni_commutes (pmon_assoc_ll (x0~~>a0) (a0~~>b0))) as qq.
69     simpl in *.
70     apply (qq _ _ g0).
71    setoid_rewrite H.
72    clear H.
74    (* rewrite using eassociativity *)
75    repeat setoid_rewrite associativity.
76    set (@eassociativity _ _ _ _ _ _ _ _ _ ec x a) as qq.
77    setoid_rewrite <- qq.
78    clear qq.
79    unfold e_v.
81    (* knock off the trailing ecomp *)
82    repeat setoid_rewrite <- associativity.
83    apply comp_respects; try reflexivity.
85    (* cancel out the adjacent assoc/cossa pair *)
86    repeat setoid_rewrite associativity.
87    setoid_rewrite juggle2.
88    etransitivity.
89    apply comp_respects; [ idtac |
90    repeat setoid_rewrite <- associativity;
91    etransitivity; [ idtac | apply left_identity ];
92    apply comp_respects; [ idtac | reflexivity ];
93    apply iso_comp1 ].
94    apply reflexivity.
96    (* now swap the order of ecomp⋉(b ~~> c) and ((x ~~> a) ⊗ (a ~~> b))⋊g *)
97    repeat setoid_rewrite associativity.
98    set (@centralmor_first) as se.
99    setoid_rewrite <- se.
100    clear se.
102    (* and knock the trailing (x ~~> b)⋊ g off *)
103    repeat setoid_rewrite <- associativity.
104    apply comp_respects; try reflexivity.
106    (* push the ecomp forward past the rlecnac *)
107    set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) (@ecomp _ _ _ _ _ _ _ _ _ ec x a b)) as qq.
108    symmetry in qq.
109    apply iso_shift_left' in qq.
110    setoid_rewrite associativity in qq.
111    symmetry in qq.
112    apply iso_shift_right' in qq.
113    simpl in qq.
114    setoid_rewrite qq.
115    clear qq.
117    (* and knock off the trailing ecomp *)
118    apply comp_respects; try reflexivity.
120    setoid_replace (iso_backward ((pmon_cancelr mn) ((x ~~> a) ⊗ (a ~~> b)))) with
121      (iso_backward ((pmon_cancelr mn) ((x ~~> a) ⊗ (a ~~> b))) >>> id _).
122    simpl.
123    set (@iso_shift_right') as ibs.
124    simpl in ibs.
125    apply ibs.
126    clear ibs.
128    setoid_rewrite (MacLane_ex_VII_1_1 (x~~>a) (a~~>b)).
129    setoid_rewrite juggle3.
130    set (fmor_preserves_comp ((x ~~> a) ⋊-)) as q.
131    simpl in q.
132    setoid_rewrite q.
133    clear q.
134    setoid_rewrite iso_comp1.
135    setoid_rewrite fmor_preserves_id.
136    setoid_rewrite right_identity.
137    apply iso_comp1.
139    (* leftovers *)
140    symmetry.
141    apply right_identity.
142    apply ecomp_central.
143    Qed.
145 Lemma underlying_associativity `{ec:ECategory(mn:=mn)(EI:=EI)(Eob:=Eob)(Ehom:=Ehom)} :
146    forall {a b : Eob} (f : EI ~~{ V }~~> a ~~> b) {c : Eob}
147    (g : EI ~~{ V }~~> b ~~> c) {d : Eob} (h : EI ~~{ V }~~> c ~~> d),
148    ((((#((pmon_cancelr mn) EI) ⁻¹ >>> (f ⋉ EI >>> (a ~~> b) ⋊ g)) >>> ecomp) ⋉ EI >>> (a ~~> c) ⋊ h)) >>> ecomp ~~
149    ((f ⋉ EI >>> (a ~~> b) ⋊ ((#((pmon_cancelr mn) EI) ⁻¹ >>> (g ⋉ EI >>> (b ~~> c) ⋊ h)) >>> ecomp))) >>> ecomp.
151   intros; symmetry; etransitivity;
152      [ setoid_rewrite associativity; apply comp_respects;
153         [ apply reflexivity | repeat setoid_rewrite associativity; apply (ecomp_is_functorial(x:=a) g h) ] | idtac ].
155   repeat setoid_rewrite <- fmor_preserves_comp.
156     repeat setoid_rewrite <- associativity.
157     apply comp_respects; try reflexivity.
158     apply comp_respects; try reflexivity.
160   set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) f) as qq.
161     apply iso_shift_right' in qq.
162     symmetry in qq.
163     setoid_rewrite <- associativity in qq.
164     apply iso_shift_left' in qq.
165     apply (fmor_respects (bin_first EI)) in qq.
166     setoid_rewrite <- fmor_preserves_comp in qq.
167     setoid_rewrite qq.
168     clear qq.
170   repeat setoid_rewrite <- fmor_preserves_comp.
171     repeat setoid_rewrite associativity.
172     apply comp_respects; try reflexivity.
174   repeat setoid_rewrite associativity.
175   set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) (@ecomp _ _ _ _ _ _ _ _ _ ec a b c)) as qq.
176     apply iso_shift_right' in qq.
177     symmetry in qq.
178     setoid_rewrite <- associativity in qq.
179     apply iso_shift_left' in qq.
180     symmetry in qq.
181     simpl in qq.
182     setoid_rewrite qq.
183     clear qq.
185   repeat setoid_rewrite <- associativity.
186     apply comp_respects; try reflexivity.
188   idtac.
189     set (iso_shift_left'
190          (iso_backward ((pmon_cancelr mn) (a ~~> b)) ⋉ EI >>> ((a ~~> b) ⋊ g) ⋉ EI) ((a ~~> b) ⋊ g)
191          (((pmon_cancelr mn) ((a ~~> b) ⊗ (b ~~> c))))) as xx.
192     symmetry.
193     etransitivity; [ apply xx | apply comp_respects; try reflexivity ].
194     clear xx.
196   setoid_rewrite (fmor_preserves_comp (bin_first EI)).
197     set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) ((iso_backward ((pmon_cancelr mn) (a ~~> b)) >>> (a ~~> b) ⋊ g))) as qq.
198     simpl in qq.
199     setoid_rewrite <- qq.
200     clear qq.
202   setoid_rewrite <- associativity.
203     setoid_rewrite iso_comp1.
204     apply left_identity.
206   Qed.
208 Instance Underlying `(ec:ECategory(mn:=mn)(EI:=EI)(Eob:=Eob)(Ehom:=Ehom)) : Category Eob (fun a b => EI~>(a~~>b)) :=
209 { id    := fun a                                  => eid a
210 ; comp  := fun a b c g f                          => #(pmon_cancelr _ _)⁻¹ >>> (g ⋉ _ >>> _ ⋊ f) >>> ecomp
211 ; eqv   := fun a b (f:EI~>(a~~>b))(g:EI~>(a~~>b)) => f ~~ g
212 }.
213   abstract (intros; apply Build_Equivalence;
214     [ unfold Reflexive
215     | unfold Symmetric
216     | unfold Transitive]; intros; simpl; auto).
217   abstract (intros; unfold Proper; unfold respectful; intros; simpl;
218   repeat apply comp_respects; try apply reflexivity;
219     [ apply (fmor_respects (bin_first EI)) | idtac ]; auto;
220     apply (fmor_respects (bin_second (a~~>b))); auto).
221   abstract (intros;
222     set (fun c d => centralmor_first(c:=c)(d:=d)(CentralMorphism:=(eid_central a))) as q;
223     setoid_rewrite q;
224     repeat setoid_rewrite associativity;
225     setoid_rewrite eleft_identity;
226     setoid_rewrite <- (ni_commutes (@pmon_cancell _ _ _ _ _ _ mn));
227     setoid_rewrite <- associativity;
228     set (coincide pmon_triangle) as qq;
229     setoid_rewrite qq;
230     simpl;
231     setoid_rewrite iso_comp2;
232     apply left_identity).
233   abstract (intros;
234     repeat setoid_rewrite associativity;
235     setoid_rewrite eright_identity;
236     setoid_rewrite <- (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn));
237     setoid_rewrite <- associativity;
238     simpl;
239     setoid_rewrite iso_comp2;
240     apply left_identity).
241   abstract (intros;
242     repeat setoid_rewrite associativity;
243     apply comp_respects; try reflexivity;
244     repeat setoid_rewrite <- associativity;
245     apply underlying_associativity).
246   Defined.
247 Coercion Underlying : ECategory >-> Category.
249 Class EFunctor
250   `{mn:PreMonoidalCat(bc:=bc)(C:=V)(I:=EI)}
251    {Eob1}{EHom1}(ec1:ECategory mn Eob1 EHom1)
252    {Eob2}{EHom2}(ec2:ECategory mn Eob2 EHom2)
253    (EFobj : Eob1 -> Eob2)
254 :=
255 { efunc_fobj           := EFobj
256 ; efunc                :  forall a b:Eob1, (a ~~> b) ~~{V}~~> ( (EFobj a) ~~> (EFobj b) )
257 ; efunc_central        :  forall a b,      CentralMorphism (efunc a b)
258 ; efunc_preserves_id   :  forall a,        eid a >>> efunc a a ~~ eid (EFobj a)
259 ; efunc_preserves_comp :  forall a b c,    (efunc a b) ⋉ _ >>>  _ ⋊ (efunc b c) >>> ecomp ~~ ecomp >>> efunc a c
260 }.
261 Coercion efunc_fobj : EFunctor >-> Funclass.
262 Implicit Arguments efunc [ Ob Hom V bin_obj' bc EI mn Eob1 EHom1 ec1 Eob2 EHom2 ec2 EFobj ].
264 Definition efunctor_id
265   `{mn:PreMonoidalCat(bc:=bc)(C:=V)(I:=EI)}
266    {Eob1}{EHom1}(ec1:ECategory mn Eob1 EHom1)
267    : EFunctor ec1 ec1 (fun x => x).
268   refine {| efunc := fun a b => id (a ~~> b) |}.
269   abstract (intros; apply Build_CentralMorphism; intros;
270     setoid_rewrite fmor_preserves_id;
271     setoid_rewrite right_identity;
272     setoid_rewrite left_identity;
273     reflexivity).
274   abstract (intros; apply right_identity).
275   abstract (intros;
276     setoid_rewrite fmor_preserves_id;
277     setoid_rewrite right_identity;
278     setoid_rewrite left_identity;
279     reflexivity).
280   Defined.
282 Definition efunctor_comp
283   `{mn:PreMonoidalCat(bc:=bc)(C:=V)(I:=EI)}
284    {Eob1}{EHom1}(ec1:ECategory mn Eob1 EHom1)
285    {Eob2}{EHom2}(ec2:ECategory mn Eob2 EHom2)
286    {Eob3}{EHom3}(ec3:ECategory mn Eob3 EHom3)
287    {Fobj}(F:EFunctor ec1 ec2 Fobj)
288    {Gobj}(G:EFunctor ec2 ec3 Gobj)
289    : EFunctor ec1 ec3 (Gobj ○ Fobj).
290   refine {| efunc := fun a b => (efunc F a b) >>> (efunc G _ _) |}; intros; simpl.
291   abstract (apply Build_CentralMorphism; intros;
292     [ set (fun a b c d => centralmor_first(CentralMorphism:=(efunc_central(EFunctor:=F)) a b)(c:=c)(d:=d)) as fc1
293     ; set (fun a b c d => centralmor_first(CentralMorphism:=(efunc_central(EFunctor:=G)) a b)(c:=c)(d:=d)) as gc1
294     ; setoid_rewrite <- (fmor_preserves_comp (-⋉d))
295     ; setoid_rewrite <- (fmor_preserves_comp (-⋉c))
296     ; setoid_rewrite <- associativity
297     ; setoid_rewrite <- fc1
298     ; setoid_rewrite    associativity
299     ; setoid_rewrite <- gc1
300     ; reflexivity
301     | set (fun a b c d => centralmor_second(CentralMorphism:=(efunc_central(EFunctor:=F)) a b)(c:=c)(d:=d)) as fc2
302     ; set (fun a b c d => centralmor_second(CentralMorphism:=(efunc_central(EFunctor:=G)) a b)(c:=c)(d:=d)) as gc2
303     ; setoid_rewrite <- (fmor_preserves_comp (d⋊-))
304     ; setoid_rewrite <- (fmor_preserves_comp (c⋊-))
305     ; setoid_rewrite <- associativity
306     ; setoid_rewrite    fc2
307     ; setoid_rewrite    associativity
308     ; setoid_rewrite    gc2
309     ; reflexivity ]).
310   abstract (setoid_rewrite <- associativity;
311     setoid_rewrite efunc_preserves_id;
312     setoid_rewrite efunc_preserves_id;
313     reflexivity).
314   abstract (repeat setoid_rewrite associativity;
315     set (fmor_preserves_comp (-⋉(b~~>c))) as q; setoid_rewrite <- q; clear q;
316     repeat setoid_rewrite associativity;
317     set (fmor_preserves_comp (((Gobj (Fobj a) ~~> Gobj (Fobj b))⋊-))) as q; setoid_rewrite <- q; clear q;
318     set (fun d e => centralmor_second(c:=d)(d:=e)(CentralMorphism:=(efunc_central(EFunctor:=F) b c))) as qq;
319     setoid_rewrite juggle2;
320     setoid_rewrite juggle2;
321     setoid_rewrite qq;
322     clear qq;
323     repeat setoid_rewrite associativity;
324     set ((efunc_preserves_comp(EFunctor:=G)) (Fobj a) (Fobj b) (Fobj c)) as q;
325     repeat setoid_rewrite associativity;
326     repeat setoid_rewrite associativity in q;
327     setoid_rewrite q;
328     clear q;
329     repeat setoid_rewrite <- associativity;
330     apply comp_respects; try reflexivity;
331     set ((efunc_preserves_comp(EFunctor:=F)) a b c) as q;
332     apply q).
333   Defined.
335 Instance UnderlyingFunctor `(EF:@EFunctor Ob Hom V bin_obj' bc EI mn Eob1 EHom1 ec1 Eob2 EHom2 ec2 Eobj)
336   : Functor (Underlying ec1) (Underlying ec2) Eobj :=
337   { fmor := fun a b (f:EI~~{V}~~>(a~~>b)) => f >>> (efunc _ a b) }.
338   abstract (intros; simpl; apply comp_respects; try reflexivity; auto).
339   abstract (intros; simpl; apply efunc_preserves_id).
340   abstract (intros;
341             simpl;
342             repeat setoid_rewrite associativity;
343             setoid_rewrite <- efunc_preserves_comp;
344             repeat setoid_rewrite associativity;
345               apply comp_respects; try reflexivity;
346             set (@fmor_preserves_comp _ _ _ _ _ _ _ (bin_first EI)) as qq;
347               setoid_rewrite <- qq;
348               clear qq;
349             repeat setoid_rewrite associativity;
350               apply comp_respects; try reflexivity;
351             repeat setoid_rewrite <- associativity;
352               apply comp_respects; try reflexivity;
353             set (@fmor_preserves_comp _ _ _ _ _ _ _ (bin_second (Eobj a ~~> Eobj b))) as qq;
354               setoid_rewrite <- qq;
355               repeat setoid_rewrite <- associativity;
356               apply comp_respects; try reflexivity;
357               clear qq;
358             apply (centralmor_first(CentralMorphism:=(efunc_central a b)))).
359   Defined.
360   Coercion UnderlyingFunctor : EFunctor >-> Functor.
362 Structure Enrichment :=
363 { enr_v_ob       : Type
364 ; enr_v_hom      : enr_v_ob -> enr_v_ob -> Type
365 ; enr_v          : Category enr_v_ob enr_v_hom
366 ; enr_v_fobj     : prod_obj enr_v enr_v -> enr_v_ob
367 ; enr_v_f        : Functor (enr_v ×× enr_v) enr_v enr_v_fobj
368 ; enr_v_i        : enr_v_ob
369 ; enr_v_mon      : MonoidalCat enr_v enr_v_fobj enr_v_f enr_v_i
370 ; enr_c_obj      : Type
371 ; enr_c_hom      : enr_c_obj -> enr_c_obj -> enr_v
372 ; enr_c          : ECategory enr_v_mon enr_c_obj enr_c_hom
373 }.
374 Coercion enr_c     : Enrichment >-> ECategory.
376 (* an enrichment for which every object of the enriching category is the tensor of finitely many hom-objects *)
377 Structure SurjectiveEnrichment :=
378 { se_enr    :  Enrichment
379 ; se_decomp :  @treeDecomposition (enr_v se_enr) (option ((enr_c_obj se_enr)*(enr_c_obj se_enr)))
380                   (fun t => match t with
381                             | None   => enr_v_i se_enr
382                             | Some x => match x with pair y z => enr_c_hom se_enr y z end
383                             end)
384                   (fun d1 d2:enr_v se_enr => enr_v_fobj se_enr (pair_obj d1 d2))
385 }.
386 Coercion se_enr  : SurjectiveEnrichment >-> Enrichment.
388 (* Enriched Fibrations *)
389 Section EFibration.
391   Context `{E:ECategory}.
392   Context  {Eob2}{Ehom2}{B:@ECategory Ob Hom V bin_obj' mn EI mn Eob2 Ehom2}.
393   Context  {efobj}(F:EFunctor E B efobj).
395   (*
396    * A morphism is prone if its image factors through the image of
397    * another morphism with the same codomain just in case the factor
398    * is the image of a unique morphism.  One might say that it
399    * "uniquely reflects factoring through morphisms with the same
400    * codomain".
401    *)
402   Definition Prone {e e'}(φ:EI~~{V}~~>(e'~~>e)) :=
403   forall e'' (ψ:EI~~{V}~~>(e''~~>e)) (g:(efobj e'')~~{B}~~>(efobj e')),
404        (comp(Category:=B) _ _ _ g (φ >>> (efunc F _ _))) ~~
405        ψ >>> (efunc F _ _)
406    ->  { χ:e''~~{E}~~>e' & ψ ~~ χ >>> φ & g ~~ comp(Category:=V) _ _ _ χ (efunc F e'' e') }.
407        (* FIXME: χ must also be unique *)
409   (* a functor is a Street Fibration if morphisms with codomain in its image are, up to iso, the images of prone morphisms *)
411   (* Street was the first to define non-evil fibrations using isomorphisms (for cleavage_pf below) rather than equality *)
412   Structure StreetCleavage (e:E)(b:B)(f:b~~{B}~~>(efobj e)) :=
413   { cleavage_e'   : E
414   ; cleavage_pf   : (efobj cleavage_e') ≅ b
415   ; cleavage_phi  : cleavage_e' ~~{E}~~> e
416   ; cleavage_cart : Prone cleavage_phi
417   ; cleavage_eqv  : #cleavage_pf >>> f  ~~ comp(Category:=V) _ _ _ cleavage_phi (efunc F _ _)
418   }.
420   (* if V, the category enriching E and B is V-enriched, we get a functor Bop->Vint *)
422   (* Every equivalence of categories is a Street fibration *)
424   (* this is actually a "Street Fibration", the non-evil version of a Grothendieck Fibration *)
425   Definition EFibration := forall e b f, exists cl:StreetCleavage e b f, True.
427   Definition ClovenEFibration := forall e b f, StreetCleavage e b f.
429   (*
430    * Now, a language has polymorphic types iff its category of
431    * judgments contains a second enriched category, the category of
432    * Kinds, and the category of types is fibered over the category of
433    * Kinds, and the weakening functor-of-fibers has a right adjoint.
434    *
435    * http://ncatlab.org/nlab/show/Grothendieck+fibration
436    *
437    * I suppose we'll need to also ask that the R-functors takes
438    * Prone morphisms to Prone morphisms.
439    *)
440 End EFibration.