87d9aa036780c12a14e2cdaf14cc81ecc46eb543
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)
23 ; eob_eob            :=  Eob
24 ; e_v                :=  mn
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
32 }.
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 EI) >>> ((- ⋉EI) \ f >>> (((a ~~> b) ⋊-) \ g >>> ecomp))) >>> ecomp ~~
38    ((x ~~> a) ⋊-) \ f >>> (ecomp >>> (#(pmon_cancelr (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.
47    apply symmetry in qq.
48    apply iso_shift_left' in qq.
49    apply symmetry in qq.
50    simpl in qq.
51    setoid_rewrite <- qq.
52    clear 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))
61     ~~
62     (#(pmon_assoc (x ~~> a) _ _)⁻¹ >>>
63      (bin_second(BinoidalCat:=bc) ((x ~~> a) ⊗ (a ~~> b))) \ g >>> #(pmon_assoc (x ~~> a) _ _))).
64     symmetry.
66     setoid_rewrite associativity.
67     symmetry.
68     apply iso_shift_right'.
69     setoid_rewrite <- pmon_coherent_l.
70     set (ni_commutes (pmon_assoc_ll (x0~~>a0) (a0~~>b0))) as qq.
71     simpl in *.
72     apply (qq _ _ g0).
73    setoid_rewrite H.
74    clear H.
76    (* rewrite using eassociativity *)
77    repeat setoid_rewrite associativity.
78    set (@eassociativity _ _ _ _ _ _ _ _ _ ec x a) as qq.
79    setoid_rewrite <- qq.
80    clear qq.
81    unfold e_v.
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.
90    etransitivity.
91    apply comp_respects; [ idtac |
92    repeat setoid_rewrite <- associativity;
93    etransitivity; [ idtac | apply left_identity ];
94    apply comp_respects; [ idtac | reflexivity ];
95    apply iso_comp1 ].
96    apply 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.
102    clear 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.
110    symmetry in qq.
111    apply iso_shift_left' in qq.
112    setoid_rewrite associativity in qq.
113    symmetry in qq.
114    apply iso_shift_right' in qq.
115    simpl in qq.
116    setoid_rewrite qq.
117    clear qq.
119    (* and knock off the trailing ecomp *)
120    apply comp_respects; try reflexivity.
122    setoid_replace (iso_backward ((pmon_cancelr) ((x ~~> a) ⊗ (a ~~> b)))) with
123      (iso_backward ((pmon_cancelr) ((x ~~> a) ⊗ (a ~~> b))) >>> id _).
124    simpl.
125    set (@iso_shift_right') as ibs.
126    simpl in ibs.
127    apply ibs.
128    clear ibs.
130    set (MacLane_ex_VII_1_1 (a~~>b) (x~~>a)) as q.
131    simpl in q.
132    setoid_rewrite <- q.
133    clear q.
134    setoid_rewrite juggle3.
135    set (fmor_preserves_comp ((x ~~> a) ⋊-)) as q.
136    simpl in q.
137    setoid_rewrite q.
138    clear q.
139    setoid_rewrite iso_comp1.
140    setoid_rewrite fmor_preserves_id.
141    setoid_rewrite right_identity.
142    apply iso_comp1.
144    (* leftovers *)
145    symmetry.
146    apply right_identity.
147    apply ecomp_central.
148    Qed.
150 Lemma underlying_associativity `{ec:ECategory(mn:=mn)(EI:=EI)(Eob:=Eob)(Ehom:=Ehom)} :
151    forall {a b : Eob} (f : EI ~~{ V }~~> a ~~> b) {c : Eob}
152    (g : EI ~~{ V }~~> b ~~> c) {d : Eob} (h : EI ~~{ V }~~> c ~~> d),
153    ((((#(pmon_cancelr EI) ⁻¹ >>> (f ⋉ EI >>> (a ~~> b) ⋊ g)) >>> ecomp) ⋉ EI >>> (a ~~> c) ⋊ h)) >>> ecomp ~~
154    ((f ⋉ EI >>> (a ~~> b) ⋊ ((#(pmon_cancelr EI) ⁻¹ >>> (g ⋉ EI >>> (b ~~> c) ⋊ h)) >>> ecomp))) >>> ecomp.
156   intros; symmetry; etransitivity;
157      [ setoid_rewrite associativity; apply comp_respects;
158         [ apply reflexivity | repeat setoid_rewrite associativity; apply (ecomp_is_functorial(x:=a) g h) ] | idtac ].
160   repeat setoid_rewrite <- fmor_preserves_comp.
161     repeat setoid_rewrite <- associativity.
162     apply comp_respects; try reflexivity.
163     apply comp_respects; try reflexivity.
165   set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) f) as qq.
166     apply iso_shift_right' in qq.
167     symmetry in qq.
168     setoid_rewrite <- associativity in qq.
169     apply iso_shift_left' in qq.
170     apply (fmor_respects (bin_first EI)) in qq.
171     setoid_rewrite <- fmor_preserves_comp in qq.
172     setoid_rewrite qq.
173     clear qq.
175   repeat setoid_rewrite <- fmor_preserves_comp.
176     repeat setoid_rewrite associativity.
177     apply comp_respects; try reflexivity.
179   repeat setoid_rewrite associativity.
180   set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) (@ecomp _ _ _ _ _ _ _ _ _ ec a b c)) as qq.
181     apply iso_shift_right' in qq.
182     symmetry in qq.
183     setoid_rewrite <- associativity in qq.
184     apply iso_shift_left' in qq.
185     symmetry in qq.
186     simpl in qq.
187     setoid_rewrite qq.
188     clear qq.
190   repeat setoid_rewrite <- associativity.
191     apply comp_respects; try reflexivity.
193   idtac.
194     set (iso_shift_left'
195          (iso_backward (pmon_cancelr (a ~~> b)) ⋉ EI >>> ((a ~~> b) ⋊ g) ⋉ EI) ((a ~~> b) ⋊ g)
196          ((pmon_cancelr ((a ~~> b) ⊗ (b ~~> c))))) as xx.
197     symmetry.
198     etransitivity; [ apply xx | apply comp_respects; try reflexivity ].
199     clear xx.
201   setoid_rewrite (fmor_preserves_comp (bin_first EI)).
202     set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) ((iso_backward (pmon_cancelr (a ~~> b)) >>> (a ~~> b) ⋊ g))) as qq.
203     simpl in qq.
204     setoid_rewrite <- qq.
205     clear qq.
207   setoid_rewrite <- associativity.
208     setoid_rewrite iso_comp1.
209     apply left_identity.
211   Qed.
213 Instance Underlying `(ec:ECategory(mn:=mn)(EI:=EI)(Eob:=Eob)(Ehom:=Ehom)) : Category Eob (fun a b => EI~>(a~~>b)) :=
214 { id    := fun a                                  => eid a
215 ; comp  := fun a b c g f                          => #(pmon_cancelr _)⁻¹ >>> (g ⋉ _ >>> _ ⋊ f) >>> ecomp
216 ; eqv   := fun a b (f:EI~>(a~~>b))(g:EI~>(a~~>b)) => f ~~ g
217 }.
218   abstract (intros; apply Build_Equivalence;
219     [ unfold Reflexive
220     | unfold Symmetric
221     | unfold Transitive]; intros; simpl; auto).
222   abstract (intros; unfold Proper; unfold respectful; intros; simpl;
223   repeat apply comp_respects; try apply reflexivity;
224     [ apply (fmor_respects (bin_first EI)) | idtac ]; auto;
225     apply (fmor_respects (bin_second (a~~>b))); auto).
226   abstract (intros;
227     set (fun c d => centralmor_first(c:=c)(d:=d)(CentralMorphism:=(eid_central a))) as q;
228     setoid_rewrite q;
229     repeat setoid_rewrite associativity;
230     setoid_rewrite eleft_identity;
231     setoid_rewrite <- (ni_commutes (@pmon_cancell _ _ _ _ _ _ mn));
232     setoid_rewrite <- associativity;
233     set (coincide pmon_triangle) as qq;
234     setoid_rewrite qq;
235     simpl;
236     setoid_rewrite iso_comp2;
237     apply left_identity).
238   abstract (intros;
239     repeat setoid_rewrite associativity;
240     setoid_rewrite eright_identity;
241     setoid_rewrite <- (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn));
242     setoid_rewrite <- associativity;
243     simpl;
244     setoid_rewrite iso_comp2;
245     apply left_identity).
246   abstract (intros;
247     repeat setoid_rewrite associativity;
248     apply comp_respects; try reflexivity;
249     repeat setoid_rewrite <- associativity;
250     apply underlying_associativity).
251   Defined.
252 Coercion Underlying : ECategory >-> Category.
254 Class EFunctor
255   `{mn:PreMonoidalCat(bc:=bc)(C:=V)(I:=EI)}
256    {Eob1}{EHom1}(ec1:ECategory mn Eob1 EHom1)
257    {Eob2}{EHom2}(ec2:ECategory mn Eob2 EHom2)
258    (EFobj : Eob1 -> Eob2)
259 :=
260 { efunc_fobj           := EFobj
261 ; efunc                :  forall a b:Eob1, (a ~~> b) ~~{V}~~> ( (EFobj a) ~~> (EFobj b) )
262 ; efunc_central        :  forall a b,      CentralMorphism (efunc a b)
263 ; efunc_preserves_id   :  forall a,        eid a >>> efunc a a ~~ eid (EFobj a)
264 ; efunc_preserves_comp :  forall a b c,    (efunc a b) ⋉ _ >>>  _ ⋊ (efunc b c) >>> ecomp ~~ ecomp >>> efunc a c
265 }.
266 Coercion efunc_fobj : EFunctor >-> Funclass.
267 Implicit Arguments efunc [ Ob Hom V bin_obj' bc EI mn Eob1 EHom1 ec1 Eob2 EHom2 ec2 EFobj ].
269 Definition efunctor_id
270   `{mn:PreMonoidalCat(bc:=bc)(C:=V)(I:=EI)}
271    {Eob1}{EHom1}(ec1:ECategory mn Eob1 EHom1)
272    : EFunctor ec1 ec1 (fun x => x).
273   refine {| efunc := fun a b => id (a ~~> b) |}.
274   abstract (intros; apply Build_CentralMorphism; intros;
275     setoid_rewrite fmor_preserves_id;
276     setoid_rewrite right_identity;
277     setoid_rewrite left_identity;
278     reflexivity).
279   abstract (intros; apply right_identity).
280   abstract (intros;
281     setoid_rewrite fmor_preserves_id;
282     setoid_rewrite right_identity;
283     setoid_rewrite left_identity;
284     reflexivity).
285   Defined.
287 Definition efunctor_comp
288   `{mn:PreMonoidalCat(bc:=bc)(C:=V)(I:=EI)}
289    {Eob1}{EHom1}(ec1:ECategory mn Eob1 EHom1)
290    {Eob2}{EHom2}(ec2:ECategory mn Eob2 EHom2)
291    {Eob3}{EHom3}(ec3:ECategory mn Eob3 EHom3)
292    {Fobj}(F:EFunctor ec1 ec2 Fobj)
293    {Gobj}(G:EFunctor ec2 ec3 Gobj)
294    : EFunctor ec1 ec3 (Gobj ○ Fobj).
295   refine {| efunc := fun a b => (efunc F a b) >>> (efunc G _ _) |}; intros; simpl.
296   abstract (apply Build_CentralMorphism; intros;
297     [ set (fun a b c d => centralmor_first(CentralMorphism:=(efunc_central(EFunctor:=F)) a b)(c:=c)(d:=d)) as fc1
298     ; set (fun a b c d => centralmor_first(CentralMorphism:=(efunc_central(EFunctor:=G)) a b)(c:=c)(d:=d)) as gc1
299     ; setoid_rewrite <- (fmor_preserves_comp (-⋉d))
300     ; setoid_rewrite <- (fmor_preserves_comp (-⋉c))
301     ; setoid_rewrite <- associativity
302     ; setoid_rewrite <- fc1
303     ; setoid_rewrite    associativity
304     ; setoid_rewrite <- gc1
305     ; reflexivity
306     | set (fun a b c d => centralmor_second(CentralMorphism:=(efunc_central(EFunctor:=F)) a b)(c:=c)(d:=d)) as fc2
307     ; set (fun a b c d => centralmor_second(CentralMorphism:=(efunc_central(EFunctor:=G)) a b)(c:=c)(d:=d)) as gc2
308     ; setoid_rewrite <- (fmor_preserves_comp (d⋊-))
309     ; setoid_rewrite <- (fmor_preserves_comp (c⋊-))
310     ; setoid_rewrite <- associativity
311     ; setoid_rewrite    fc2
312     ; setoid_rewrite    associativity
313     ; setoid_rewrite    gc2
314     ; reflexivity ]).
315   abstract (setoid_rewrite <- associativity;
316     setoid_rewrite efunc_preserves_id;
317     setoid_rewrite efunc_preserves_id;
318     reflexivity).
319   abstract (repeat setoid_rewrite associativity;
320     set (fmor_preserves_comp (-⋉(b~~>c))) as q; setoid_rewrite <- q; clear q;
321     repeat setoid_rewrite associativity;
322     set (fmor_preserves_comp (((Gobj (Fobj a) ~~> Gobj (Fobj b))⋊-))) as q; setoid_rewrite <- q; clear q;
323     set (fun d e => centralmor_second(c:=d)(d:=e)(CentralMorphism:=(efunc_central(EFunctor:=F) b c))) as qq;
324     setoid_rewrite juggle2;
325     setoid_rewrite juggle2;
326     setoid_rewrite qq;
327     clear qq;
328     repeat setoid_rewrite associativity;
329     set ((efunc_preserves_comp(EFunctor:=G)) (Fobj a) (Fobj b) (Fobj c)) as q;
330     repeat setoid_rewrite associativity;
331     repeat setoid_rewrite associativity in q;
332     setoid_rewrite q;
333     clear q;
334     repeat setoid_rewrite <- associativity;
335     apply comp_respects; try reflexivity;
336     set ((efunc_preserves_comp(EFunctor:=F)) a b c) as q;
337     apply q).
338   Defined.
340 Instance UnderlyingFunctor `(EF:@EFunctor Ob Hom V bin_obj' bc EI mn Eob1 EHom1 ec1 Eob2 EHom2 ec2 Eobj)
341   : Functor (Underlying ec1) (Underlying ec2) Eobj :=
342   { fmor := fun a b (f:EI~~{V}~~>(a~~>b)) => f >>> (efunc _ a b) }.
343   abstract (intros; simpl; apply comp_respects; try reflexivity; auto).
344   abstract (intros; simpl; apply efunc_preserves_id).
345   abstract (intros;
346             simpl;
347             repeat setoid_rewrite associativity;
348             setoid_rewrite <- efunc_preserves_comp;
349             repeat setoid_rewrite associativity;
350               apply comp_respects; try reflexivity;
351             set (@fmor_preserves_comp _ _ _ _ _ _ _ (bin_first EI)) as qq;
352               setoid_rewrite <- qq;
353               clear qq;
354             repeat setoid_rewrite associativity;
355               apply comp_respects; try reflexivity;
356             repeat setoid_rewrite <- associativity;
357               apply comp_respects; try reflexivity;
358             set (@fmor_preserves_comp _ _ _ _ _ _ _ (bin_second (Eobj a ~~> Eobj b))) as qq;
359               setoid_rewrite <- qq;
360               repeat setoid_rewrite <- associativity;
361               apply comp_respects; try reflexivity;
362               clear qq;
363             apply (centralmor_first(CentralMorphism:=(efunc_central a b)))).
364   Defined.
365   Coercion UnderlyingFunctor : EFunctor >-> Functor.
367 Class EBinoidalCat `(ec:ECategory) :=
368 { ebc_bobj   :  ec -> ec -> ec
369 ; ebc_first  :  forall a:ec, EFunctor ec ec (fun x => ebc_bobj x a)
370 ; ebc_second :  forall a:ec, EFunctor ec ec (fun x => ebc_bobj a x)
371 ; ebc_ec     := ec  (* this isn't a coercion - avoids duplicate paths *)
372 }.
374 Instance EBinoidalCat_is_binoidal `(ebc:EBinoidalCat(ec:=ec)) : BinoidalCat (Underlying ec) ebc_bobj.
375   apply Build_BinoidalCat.
376   apply (fun a => UnderlyingFunctor (ebc_first a)).
377   apply (fun a => UnderlyingFunctor (ebc_second a)).
378   Defined.
380 Coercion EBinoidalCat_is_binoidal : EBinoidalCat >-> BinoidalCat.
382 (* Enriched Fibrations *)
383 Section EFibration.
385   Context `{E:ECategory}.
386   Context  {Eob2}{Ehom2}{B:@ECategory Ob Hom V bin_obj' mn EI mn Eob2 Ehom2}.
387   Context  {efobj}(F:EFunctor E B efobj).
389   (*
390    * A morphism is prone if its image factors through the image of
391    * another morphism with the same codomain just in case the factor
392    * is the image of a unique morphism.  One might say that it
393    * "uniquely reflects factoring through morphisms with the same
394    * codomain".
395    *)
396   Definition Prone {e e'}(φ:EI~~{V}~~>(e'~~>e)) :=
397   forall e'' (ψ:EI~~{V}~~>(e''~~>e)) (g:(efobj e'')~~{B}~~>(efobj e')),
398        (comp(Category:=B) _ _ _ g (φ >>> (efunc F _ _))) ~~
399        ψ >>> (efunc F _ _)
400    ->  { χ:e''~~{E}~~>e' & ψ ~~ χ >>> φ & g ~~ comp(Category:=V) _ _ _ χ (efunc F e'' e') }.
401        (* FIXME: χ must also be unique *)
403   (* a functor is a Street Fibration if morphisms with codomain in its image are, up to iso, the images of prone morphisms *)
405   (* Street was the first to define non-evil fibrations using isomorphisms (for cleavage_pf below) rather than equality *)
406   Structure StreetCleavage (e:E)(b:B)(f:b~~{B}~~>(efobj e)) :=
407   { cleavage_e'   : E
408   ; cleavage_pf   : (efobj cleavage_e') ≅ b
409   ; cleavage_phi  : cleavage_e' ~~{E}~~> e
410   ; cleavage_cart : Prone cleavage_phi
411   ; cleavage_eqv  : #cleavage_pf >>> f  ~~ comp(Category:=V) _ _ _ cleavage_phi (efunc F _ _)
412   }.
414   (* if V, the category enriching E and B is V-enriched, we get a functor Bop->Vint *)
416   (* Every equivalence of categories is a Street fibration *)
418   (* this is actually a "Street Fibration", the non-evil version of a Grothendieck Fibration *)
419   Definition EFibration := forall e b f, exists cl:StreetCleavage e b f, True.
421   Definition ClovenEFibration := forall e b f, StreetCleavage e b f.
423   (*
424    * Now, a language has polymorphic types iff its category of
425    * judgments contains a second enriched category, the category of
426    * Kinds, and the category of types is fibered over the category of
427    * Kinds, and the weakening functor-of-fibers has a right adjoint.
428    *
429    * http://ncatlab.org/nlab/show/Grothendieck+fibration
430    *
431    * I suppose we'll need to also ask that the R-functors takes
432    * Prone morphisms to Prone morphisms.
433    *)
434 End EFibration.