Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
-Require Import ProductCategories_ch1_6_1.
Require Import Subcategories_ch7_1.
(******************************************************************************)
}.
Notation "f × g" := (commutative_morprod f g).
-Section BinoidalCat_from_Bifunctor.
- Context `{C:Category}{Fobj}(F:Functor (C ×× C) C Fobj).
- Definition BinoidalCat_from_Bifunctor_first (a:C) : Functor C C (fun b => Fobj (pair_obj b a)).
- apply Build_Functor with (fmor:=(fun a0 b (f:a0~~{C}~~>b) =>
- @fmor _ _ _ _ _ _ _ F (pair_obj a0 a) (pair_obj b a) (pair_mor (pair_obj a0 a) (pair_obj b a) f (id a)))); intros; simpl;
- [ abstract (set (fmor_respects(F)) as q; apply q; split; simpl; auto)
- | abstract (set (fmor_preserves_id(F)) as q; apply q)
- | abstract (etransitivity;
- [ set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q; apply q
- | set (fmor_respects(F)) as q; apply q ];
- split; simpl; auto) ].
- Defined.
- Definition BinoidalCat_from_Bifunctor_second (a:C) : Functor C C (fun b => Fobj (pair_obj a b)).
- apply Build_Functor with (fmor:=(fun a0 b (f:a0~~{C}~~>b) =>
- @fmor _ _ _ _ _ _ _ F (pair_obj a a0) (pair_obj a b) (pair_mor (pair_obj a a0) (pair_obj a b) (id a) f))); intros;
- [ abstract (set (fmor_respects(F)) as q; apply q; split; simpl; auto)
- | abstract (set (fmor_preserves_id(F)) as q; apply q)
- | abstract (etransitivity;
- [ set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q; apply q
- | set (fmor_respects(F)) as q; apply q ];
- split; simpl; auto) ].
- Defined.
-
- Definition BinoidalCat_from_Bifunctor : BinoidalCat C (fun a b => Fobj (pair_obj a b)).
- refine {| bin_first := BinoidalCat_from_Bifunctor_first
- ; bin_second := BinoidalCat_from_Bifunctor_second
- |}.
- Defined.
-
- Lemma Bifunctors_Create_Commutative_Binoidal_Categories : CommutativeCat BinoidalCat_from_Bifunctor.
- abstract (intros; apply Build_CommutativeCat; intros; apply Build_CentralMorphism; intros; simpl; (
- etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ]; symmetry;
- etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ];
- apply (fmor_respects(F));
- split;
- [ etransitivity; [ apply left_identity | symmetry; apply right_identity ]
- | etransitivity; [ apply right_identity | symmetry; apply left_identity ] ])).
- Defined.
-
-End BinoidalCat_from_Bifunctor.
; eid_central : forall a, CentralMorphism (eid a)
; ecomp : forall {a b c}, (a~~>b)⊗(b~~>c) ~> (a~~>c)
; ecomp_central :> forall {a b c}, CentralMorphism (@ecomp a b c)
-; eleft_identity : forall {a b }, eid a ⋉ (a~~>b) >>> ecomp ~~ #(pmon_cancell _ _)
-; eright_identity : forall {a b }, (a~~>b) ⋊ eid b >>> ecomp ~~ #(pmon_cancelr _ _)
-; eassociativity : forall {a b c d}, #(pmon_assoc _ _ _ (_~~>_))⁻¹ >>> ecomp ⋉ (c~~>d) >>> ecomp ~~ (a~~>b) ⋊ ecomp >>> ecomp
+; eleft_identity : forall {a b }, eid a ⋉ (a~~>b) >>> ecomp ~~ #(pmon_cancell _)
+; eright_identity : forall {a b }, (a~~>b) ⋊ eid b >>> ecomp ~~ #(pmon_cancelr _)
+; eassociativity : forall {a b c d}, #(pmon_assoc _ _ (_~~>_))⁻¹ >>> ecomp ⋉ (c~~>d) >>> ecomp ~~ (a~~>b) ⋊ ecomp >>> ecomp
}.
Notation "a ~~> b" := (@ehom _ _ _ _ _ _ _ _ _ _ a b) : category_scope.
Coercion eob_eob : ECategory >-> Sortclass.
Lemma ecomp_is_functorial `{ec:ECategory}{a b c}{x}(f:EI~~{V}~~>(a~~>b))(g:EI~~{V}~~>(b~~>c)) :
- ((x ~~> a) ⋊-) \ (iso_backward ((pmon_cancelr mn) EI) >>> ((- ⋉EI) \ f >>> (((a ~~> b) ⋊-) \ g >>> ecomp))) >>> ecomp ~~
- ((x ~~> a) ⋊-) \ f >>> (ecomp >>> (#((pmon_cancelr mn) (x ~~> b)) ⁻¹ >>> (((x ~~> b) ⋊-) \ g >>> ecomp))).
+ ((x ~~> a) ⋊-) \ (iso_backward (pmon_cancelr EI) >>> ((- ⋉EI) \ f >>> (((a ~~> b) ⋊-) \ g >>> ecomp))) >>> ecomp ~~
+ ((x ~~> a) ⋊-) \ f >>> (ecomp >>> (#(pmon_cancelr (x ~~> b)) ⁻¹ >>> (((x ~~> b) ⋊-) \ g >>> ecomp))).
set (@fmor_preserves_comp) as fmor_preserves_comp'.
assert (forall {a b c x}(g:EI~~{V}~~>(b ~~> c)),
((bin_second(BinoidalCat:=bc) (x ~~> a)) \ ((bin_second(BinoidalCat:=bc) (a ~~> b)) \ g))
~~
- (#(pmon_assoc mn (x ~~> a) _ _)⁻¹ >>>
- (bin_second(BinoidalCat:=bc) ((x ~~> a) ⊗ (a ~~> b))) \ g >>> #(pmon_assoc mn (x ~~> a) _ _))).
+ (#(pmon_assoc (x ~~> a) _ _)⁻¹ >>>
+ (bin_second(BinoidalCat:=bc) ((x ~~> a) ⊗ (a ~~> b))) \ g >>> #(pmon_assoc (x ~~> a) _ _))).
symmetry.
setoid_rewrite associativity.
(* and knock off the trailing ecomp *)
apply comp_respects; try reflexivity.
- setoid_replace (iso_backward ((pmon_cancelr mn) ((x ~~> a) ⊗ (a ~~> b)))) with
- (iso_backward ((pmon_cancelr mn) ((x ~~> a) ⊗ (a ~~> b))) >>> id _).
+ setoid_replace (iso_backward ((pmon_cancelr) ((x ~~> a) ⊗ (a ~~> b)))) with
+ (iso_backward ((pmon_cancelr) ((x ~~> a) ⊗ (a ~~> b))) >>> id _).
simpl.
set (@iso_shift_right') as ibs.
simpl in ibs.
Lemma underlying_associativity `{ec:ECategory(mn:=mn)(EI:=EI)(Eob:=Eob)(Ehom:=Ehom)} :
forall {a b : Eob} (f : EI ~~{ V }~~> a ~~> b) {c : Eob}
(g : EI ~~{ V }~~> b ~~> c) {d : Eob} (h : EI ~~{ V }~~> c ~~> d),
- ((((#((pmon_cancelr mn) EI) ⁻¹ >>> (f ⋉ EI >>> (a ~~> b) ⋊ g)) >>> ecomp) ⋉ EI >>> (a ~~> c) ⋊ h)) >>> ecomp ~~
- ((f ⋉ EI >>> (a ~~> b) ⋊ ((#((pmon_cancelr mn) EI) ⁻¹ >>> (g ⋉ EI >>> (b ~~> c) ⋊ h)) >>> ecomp))) >>> ecomp.
+ ((((#(pmon_cancelr EI) ⁻¹ >>> (f ⋉ EI >>> (a ~~> b) ⋊ g)) >>> ecomp) ⋉ EI >>> (a ~~> c) ⋊ h)) >>> ecomp ~~
+ ((f ⋉ EI >>> (a ~~> b) ⋊ ((#(pmon_cancelr EI) ⁻¹ >>> (g ⋉ EI >>> (b ~~> c) ⋊ h)) >>> ecomp))) >>> ecomp.
intros; symmetry; etransitivity;
[ setoid_rewrite associativity; apply comp_respects;
idtac.
set (iso_shift_left'
- (iso_backward ((pmon_cancelr mn) (a ~~> b)) ⋉ EI >>> ((a ~~> b) ⋊ g) ⋉ EI) ((a ~~> b) ⋊ g)
- (((pmon_cancelr mn) ((a ~~> b) ⊗ (b ~~> c))))) as xx.
+ (iso_backward (pmon_cancelr (a ~~> b)) ⋉ EI >>> ((a ~~> b) ⋊ g) ⋉ EI) ((a ~~> b) ⋊ g)
+ ((pmon_cancelr ((a ~~> b) ⊗ (b ~~> c))))) as xx.
symmetry.
etransitivity; [ apply xx | apply comp_respects; try reflexivity ].
clear xx.
setoid_rewrite (fmor_preserves_comp (bin_first EI)).
- set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) ((iso_backward ((pmon_cancelr mn) (a ~~> b)) >>> (a ~~> b) ⋊ g))) as qq.
+ set (ni_commutes (@pmon_cancelr _ _ _ _ _ _ mn) ((iso_backward (pmon_cancelr (a ~~> b)) >>> (a ~~> b) ⋊ g))) as qq.
simpl in qq.
setoid_rewrite <- qq.
clear qq.
Instance Underlying `(ec:ECategory(mn:=mn)(EI:=EI)(Eob:=Eob)(Ehom:=Ehom)) : Category Eob (fun a b => EI~>(a~~>b)) :=
{ id := fun a => eid a
-; comp := fun a b c g f => #(pmon_cancelr _ _)⁻¹ >>> (g ⋉ _ >>> _ ⋊ f) >>> ecomp
+; comp := fun a b c g f => #(pmon_cancelr _)⁻¹ >>> (g ⋉ _ >>> _ ⋊ f) >>> ecomp
; eqv := fun a b (f:EI~>(a~~>b))(g:EI~>(a~~>b)) => f ~~ g
}.
abstract (intros; apply Build_Equivalence;
Defined.
Coercion UnderlyingFunctor : EFunctor >-> Functor.
-Structure Enrichment :=
-{ enr_v_ob : Type
-; enr_v_hom : enr_v_ob -> enr_v_ob -> Type
-; enr_v : Category enr_v_ob enr_v_hom
-; enr_v_fobj : prod_obj enr_v enr_v -> enr_v_ob
-; enr_v_f : Functor (enr_v ×× enr_v) enr_v enr_v_fobj
-; enr_v_i : enr_v_ob
-; enr_v_mon : MonoidalCat enr_v enr_v_fobj enr_v_f enr_v_i
-; enr_c_obj : Type
-; enr_c_hom : enr_c_obj -> enr_c_obj -> enr_v
-; enr_c : ECategory enr_v_mon enr_c_obj enr_c_hom
+Class EBinoidalCat `(ec:ECategory) :=
+{ ebc_bobj : ec -> ec -> ec
+; ebc_first : forall a:ec, EFunctor ec ec (fun x => ebc_bobj x a)
+; ebc_second : forall a:ec, EFunctor ec ec (fun x => ebc_bobj a x)
}.
-Coercion enr_c : Enrichment >-> ECategory.
-
-(* an enrichment for which every object of the enriching category is the tensor of finitely many hom-objects *)
-Structure SurjectiveEnrichment (e:Enrichment) :=
-{ se_enr := e
-; se_decomp : @treeDecomposition (enr_v e) (option ((enr_c_obj e)*(enr_c_obj e)))
- (fun t => match t with
- | None => enr_v_i e
- | Some x => match x with pair y z => enr_c_hom e y z end
- end)
- (fun d1 d2:enr_v e => enr_v_fobj e (pair_obj d1 d2))
-}.
-Coercion se_enr : SurjectiveEnrichment >-> Enrichment.
+
+Instance EBinoidalCat_is_binoidal `(ebc:EBinoidalCat(ec:=ec)) : BinoidalCat (Underlying ec) ebc_bobj.
+ apply Build_BinoidalCat.
+ apply (fun a => UnderlyingFunctor (ebc_first a)).
+ apply (fun a => UnderlyingFunctor (ebc_second a)).
+ Defined.
+
+Coercion EBinoidalCat_is_binoidal : EBinoidalCat >-> BinoidalCat.
(* Enriched Fibrations *)
Section EFibration.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
+Require Import NaturalIsomorphisms_ch7_5.
(* Definition 7.24 *)
Class EquivalentCategories `(C:Category)`(D:Category){Fobj}{Gobj}(F:Functor C D Fobj)(G:Functor D C Gobj) :=
Require Import NaturalTransformations_ch7_4.
Require Import NaturalIsomorphisms_ch7_5.
Require Import Coherence_ch7_8.
+Require Import BinoidalCategories.
+Require Import PreMonoidalCategories.
+Require Import PreMonoidalCenter.
Require Import MonoidalCategories_ch7_8.
(* A Freyd Category is... *)
Class FreydCategory
(* a cartesian category C *)
- `(C:CartesianCat(Ob:=Ob)(C:=C1)(Fobj:=fun x => bobj (fst_obj _ _ x) (snd_obj _ _ x)))
+ `(C:CartesianCat(Ob:=Ob)(C:=C1))
(* a premonoidal category K with the same objects (its unit object is 1 because the functor is both IIO and strict) *)
`(K:PreMonoidalCat(Ob:=Ob)(bin_obj':=bobj)(I:=@one _ _ _ C))
(* an identity-on-objects functor J:C->Z(K) *)
-:= { fc_J : Functor C (CenterMonoidal K) (fun x => exist _ x I)
+:= { fc_J : Functor C (Center_is_Monoidal K) (fun x => exist (fun _ => True) x I)
(* which is not only monoidal *)
- ; fc_mf_J : MonoidalFunctor C (CenterMonoidal K) fc_J
+ ; fc_mf_J : MonoidalFunctor C (Center_is_Monoidal K) fc_J
- (* but in fact strict (meaning the functor's coherence maps are identities) *)
- ; fc_strict : forall a, iso_forward (mf_coherence fc_mf_J a) ~~ id _
+ (* but in fact strict (meaning the functor's coherence maps are identities) *)
+ (*; fc_strict : forall a b, #(mf_first a b) ~~ id _
+ FIXME - I will need to separate Subcategory from FullSubCategory in order to fix this *)
; fc_C := C
; fc_K := K
Require Import NaturalIsomorphisms_ch7_5.
Require Import FunctorCategories_ch7_7.
Require Import Coherence_ch7_8.
+
+Require Import PreMonoidalCategories.
+Require Import BinoidalCategories.
Require Import MonoidalCategories_ch7_8.
+Require Import PreMonoidalCenter.
Require Import Exponentials_ch6.
-(*Require Import CategoryOfCategories_ch7_1.*)
Require Import Yoneda_ch8.
Require Import Adjoints_ch9.
+(*Require Import CategoryOfCategories_ch7_1.*)
(*Require Import PolynomialCategories.*)
(*Require Import CoqCategory.*)
-(*Require Import NaturalDeduction.*)
-(*Require Import NaturalDeductionCategories.*)
(*Require Import CartesianEnrichmentsHaveMonoidalHomFunctors.*)
-(*Require Import Reification.*)
-(*Require Import GeneralizedArrow.*)
-(*Require Import ReificationFromGArrow.*)
-(*Require Import GArrowFromReification.*)
-(*Require Import Roundtrip.*)
-(*Require Import RoundtripSlides.*)
+
+Require Import RepresentableStructure_ch7_2.
+
+Require Import EquivalentCategories_ch7_8.
+Require Import FreydAFT_ch9_8.
+Require Import KanExtension_ch9_6.
+Require Import LCCCs_ch9_7.
+Require Import Monads_ch10.
+Require Import NaturalNumbersObject_ch9_8.
+Require Import Presheaves_ch9_7.
(* very slow! *)
-(*Require Import FreydCategories.*)
+Require Import FreydCategories.
(*Require Import Arrows.*)
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
-Require Import ProductCategories_ch1_6_1.
Require Import InitialTerminal_ch2_2.
Require Import Subcategories_ch7_1.
+Require Import ProductCategories_ch1_6_1.
Require Import NaturalTransformations_ch7_4.
Require Import NaturalIsomorphisms_ch7_5.
Require Import Coherence_ch7_8.
(* Chapter 7.8: Monoidal Categories *)
(******************************************************************************)
-Class MonoidalCat `{C:Category}{Fobj:prod_obj C C -> C}{F:Functor (C ×× C) C Fobj}(I:C) :=
-{ mon_f := F
-; mon_i := I
-; mon_c := C
-; mon_first := fun a b c (f:a~>b) => F \ pair_mor (pair_obj a c) (pair_obj b c) f (id c)
-; mon_second := fun a b c (f:a~>b) => F \ pair_mor (pair_obj c a) (pair_obj c b) (id c) f
-; mon_cancelr : (func_rlecnac I >>>> F) <~~~> functor_id C
-; mon_cancell : (func_llecnac I >>>> F) <~~~> functor_id C
-; mon_assoc : ((F **** (functor_id C)) >>>> F) <~~~> func_cossa >>>> ((((functor_id C) **** F) >>>> F))
-; mon_pentagon : Pentagon mon_first mon_second (fun a b c => #(mon_assoc (pair_obj (pair_obj a b) c)))
-; mon_triangle : Triangle mon_first mon_second (fun a b c => #(mon_assoc (pair_obj (pair_obj a b) c)))
- (fun a => #(mon_cancell a)) (fun a => #(mon_cancelr a))
-}.
-(* Coq manual on coercions: ... only the oldest one is valid and the
- * others are ignored. So the order of declaration of coercions is
- * important. *)
-Coercion mon_c : MonoidalCat >-> Category.
-Coercion mon_f : MonoidalCat >-> Functor.
-Implicit Arguments mon_f [Ob Hom C Fobj F I].
-Implicit Arguments mon_i [Ob Hom C Fobj F I].
-Implicit Arguments mon_c [Ob Hom C Fobj F I].
-Implicit Arguments MonoidalCat [Ob Hom ].
-
(* TO DO: show that the endofunctors on any given category form a monoidal category *)
-Section MonoidalFunctor.
- Context `(m1:MonoidalCat(C:=C1)) `(m2:MonoidalCat(C:=C2)).
- Class MonoidalFunctor {Mobj:C1->C2} (mf_F:Functor C1 C2 Mobj) :=
- { mf_f := mf_F where "f ⊕⊕ g" := (@fmor _ _ _ _ _ _ _ m2 _ _ (pair_mor (pair_obj _ _) (pair_obj _ _) f g))
- ; mf_coherence : (mf_F **** mf_F) >>>> (mon_f m2) <~~~> (mon_f m1) >>>> mf_F
- ; mf_phi := fun a b => #(mf_coherence (pair_obj a b))
- ; mf_id : (mon_i m2) ≅ (mf_F (mon_i m1))
- ; mf_cancelr : forall a, #(mon_cancelr(MonoidalCat:=m2) (mf_F a)) ~~
- (id (mf_F a)) ⊕⊕ #mf_id >>> mf_phi a (mon_i _) >>> mf_F \ #(mon_cancelr a)
- ; mf_cancell : forall b, #(mon_cancell (mf_F b)) ~~
- #mf_id ⊕⊕ (id (mf_F b)) >>> mf_phi (mon_i _) b >>> mf_F \ #(mon_cancell b)
- ; mf_assoc : forall a b c, (mf_phi a b) ⊕⊕ (id (mf_F c)) >>> (mf_phi _ c) >>>
- (mf_F \ #(mon_assoc (pair_obj (pair_obj a b) c) )) ~~
- #(mon_assoc (pair_obj (pair_obj _ _) _) ) >>>
- (id (mf_F a)) ⊕⊕ (mf_phi b c) >>> (mf_phi a _)
- }.
-End MonoidalFunctor.
-Coercion mf_f : MonoidalFunctor >-> Functor.
-Implicit Arguments mf_coherence [ Ob Hom C1 Fobj F I0 m1 Ob0 Hom0 C2 Fobj0 F0 I1 m2 Mobj mf_F ].
-Implicit Arguments mf_id [ Ob Hom C1 Fobj F I0 m1 Ob0 Hom0 C2 Fobj0 F0 I1 m2 Mobj mf_F ].
-Section MonoidalFunctorsCompose.
- Context `(m1:MonoidalCat).
- Context `(m2:MonoidalCat).
- Context `(m3:MonoidalCat).
- Context {f1obj}(f1:@Functor _ _ m1 _ _ m2 f1obj).
- Context {f2obj}(f2:@Functor _ _ m2 _ _ m3 f2obj).
- Context (mf1:MonoidalFunctor m1 m2 f1).
- Context (mf2:MonoidalFunctor m2 m3 f2).
+(*
+ * Unlike Awodey, I define a monoidal category to be a premonoidal
+ * category in which all morphisms are central. This is partly to
+ * have a clean inheritance hierarchy, but also because Coq bogs down
+ * on product categories for some inexplicable reason.
+ *)
+Class MonoidalCat `(pm:PreMonoidalCat) :=
+{ mon_pm := pm
+; mon_commutative :> CommutativeCat pm
+}.
+Coercion mon_pm : MonoidalCat >-> PreMonoidalCat.
+Coercion mon_commutative : MonoidalCat >-> CommutativeCat.
+
+(* a monoidal functor is just a premonoidal functor between premonoidal categories which happen to be monoidal *)
+Definition MonoidalFunctor `(m1:MonoidalCat) `(m2:MonoidalCat) := PreMonoidalFunctor m1 m2.
+
+Definition MonoidalFunctorsCompose
+ `{M1 :MonoidalCat(C:=C1)}
+ `{M2 :MonoidalCat(C:=C2)}
+ {fobj12:C1 -> C2 }
+ (MF12 :MonoidalFunctor M1 M2 fobj12)
+ `{M3 :MonoidalCat(C:=C3)}
+ {fobj23:C2 -> C3 }
+ (MF23 :MonoidalFunctor M2 M3 fobj23)
+ : MonoidalFunctor M1 M3 (fobj23 ○ fobj12).
+ apply PreMonoidalFunctorsCompose.
+ apply MF12.
+ apply MF23.
+ Defined.
- Lemma mf_compose_coherence : (f1 >>>> f2) **** (f1 >>>> f2) >>>> m3 <~~~> m1 >>>> (f1 >>>> f2).
- set (mf_coherence mf1) as mc1.
- set (mf_coherence mf2) as mc2.
- set (@ni_comp) as q.
- set (q _ _ _ _ _ _ _ ((f1 >>>> f2) **** (f1 >>>> f2) >>>> m3) _ ((f1 **** f1 >>>> m2) >>>> f2) _ (m1 >>>> (f1 >>>> f2))) as qq.
- apply qq; clear qq; clear q.
- apply (@ni_comp _ _ _ _ _ _ _ _ _ (f1 **** f1 >>>> (f2 **** f2 >>>> m3)) _ _).
- apply (@ni_comp _ _ _ _ _ _ _ _ _ ((f1 **** f1 >>>> f2 **** f2) >>>> m3) _ _).
- eapply ni_respects.
- apply ni_prod_comp.
- apply ni_id.
- apply ni_associativity.
- apply ni_inv.
- eapply ni_comp.
- apply (ni_associativity (f1 **** f1) m2 f2).
- apply (ni_respects (F0:=f1 **** f1)(F1:=f1 **** f1)(G0:=(m2 >>>> f2))(G1:=(f2 **** f2 >>>> m3))).
- apply ni_id.
- apply ni_inv.
- apply mc2.
- apply ni_inv.
- eapply ni_comp.
- eapply ni_inv.
- apply (ni_associativity m1 f1 f2).
- apply ni_respects.
- apply ni_inv.
- apply mc1.
- apply ni_id.
+Section BinoidalCat_from_Bifunctor.
+ Context `{C:Category}{Fobj}(F:Functor (C ×× C) C Fobj).
+ Definition BinoidalCat_from_Bifunctor_first (a:C) : Functor C C (fun b => Fobj (pair_obj b a)).
+ apply Build_Functor with (fmor:=(fun a0 b (f:a0~~{C}~~>b) =>
+ @fmor _ _ _ _ _ _ _ F (pair_obj a0 a) (pair_obj b a) (pair_mor (pair_obj a0 a) (pair_obj b a) f (id a)))); intros; simpl;
+ [ abstract (set (fmor_respects(F)) as q; apply q; split; simpl; auto)
+ | abstract (set (fmor_preserves_id(F)) as q; apply q)
+ | abstract (etransitivity;
+ [ set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q; apply q
+ | set (fmor_respects(F)) as q; apply q ];
+ split; simpl; auto) ].
+ Defined.
+ Definition BinoidalCat_from_Bifunctor_second (a:C) : Functor C C (fun b => Fobj (pair_obj a b)).
+ apply Build_Functor with (fmor:=(fun a0 b (f:a0~~{C}~~>b) =>
+ @fmor _ _ _ _ _ _ _ F (pair_obj a a0) (pair_obj a b) (pair_mor (pair_obj a a0) (pair_obj a b) (id a) f))); intros;
+ [ abstract (set (fmor_respects(F)) as q; apply q; split; simpl; auto)
+ | abstract (set (fmor_preserves_id(F)) as q; apply q)
+ | abstract (etransitivity;
+ [ set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q; apply q
+ | set (fmor_respects(F)) as q; apply q ];
+ split; simpl; auto) ].
Defined.
- Instance MonoidalFunctorsCompose : MonoidalFunctor m1 m3 (f1 >>>> f2) :=
- { mf_id := id_comp (mf_id mf2) (functors_preserve_isos f2 (mf_id mf1))
- ; mf_coherence := mf_compose_coherence
- }.
- admit.
- admit.
- admit.
+ Definition BinoidalCat_from_Bifunctor : BinoidalCat C (fun a b => Fobj (pair_obj a b)).
+ refine {| bin_first := BinoidalCat_from_Bifunctor_first
+ ; bin_second := BinoidalCat_from_Bifunctor_second
+ |}.
+ Defined.
+
+ Lemma Bifunctors_Create_Commutative_Binoidal_Categories : CommutativeCat BinoidalCat_from_Bifunctor.
+ abstract (intros; apply Build_CommutativeCat; intros; apply Build_CentralMorphism; intros; simpl; (
+ etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ]; symmetry;
+ etransitivity; [ apply (fmor_preserves_comp(F)) | idtac ];
+ apply (fmor_respects(F));
+ split;
+ [ etransitivity; [ apply left_identity | symmetry; apply right_identity ]
+ | etransitivity; [ apply right_identity | symmetry; apply left_identity ] ])).
Defined.
-End MonoidalFunctorsCompose.
+ (* if this binoidal structure has all of the natural isomorphisms of a premonoidal category, then it's monoidal *)
+ Context {pmI}(pm:PreMonoidalCat BinoidalCat_from_Bifunctor pmI).
-Section MonoidalCat_is_PreMonoidal.
- Context `(M:MonoidalCat).
- Definition mon_bin_M := BinoidalCat_from_Bifunctor (mon_f M).
- Existing Instance mon_bin_M.
+ Instance PreMonoidalCat_from_bifunctor_is_Monoidal : MonoidalCat pm :=
+ { mon_commutative := Bifunctors_Create_Commutative_Binoidal_Categories
+ }.
- Lemma mon_pmon_assoc : forall a b, (bin_second a >>>> bin_first b) <~~~> (bin_first b >>>> bin_second a).
- intros.
- set (fun c => mon_assoc (pair_obj (pair_obj a c) b)) as qq.
- simpl in qq.
- apply Build_NaturalIsomorphism with (ni_iso:=qq).
- abstract (intros; set ((ni_commutes mon_assoc) (pair_obj (pair_obj a A) b) (pair_obj (pair_obj a B) b)
- (pair_mor (pair_obj (pair_obj a A) b) (pair_obj (pair_obj a B) b)
- (pair_mor (pair_obj a A) (pair_obj a B) (id a) f) (id b))) as qr;
- apply qr).
- Defined.
+End BinoidalCat_from_Bifunctor.
- Lemma mon_pmon_assoc_rr : forall a b, (bin_first (a⊗b)) <~~~> (bin_first a >>>> bin_first b).
- intros.
- set (fun c:C => mon_assoc (pair_obj (pair_obj c a) b)) as qq.
- simpl in qq.
- apply ni_inv.
- apply Build_NaturalIsomorphism with (ni_iso:=qq).
- abstract (intros; set ((ni_commutes mon_assoc) (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
- (pair_mor (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
- (pair_mor (pair_obj _ _) (pair_obj _ _) f (id a)) (id b))) as qr;
- etransitivity; [ idtac | apply qr ];
- apply comp_respects; try reflexivity;
- unfold mon_f;
- simpl;
- apply ((fmor_respects F) (pair_obj _ _) (pair_obj _ _));
- split; try reflexivity;
- symmetry;
- simpl;
- set (@fmor_preserves_id _ _ _ _ _ _ _ F (pair_obj a b)) as qqqq;
- simpl in qqqq;
- apply qqqq).
- Defined.
- Lemma mon_pmon_assoc_ll : forall a b, (bin_second (a⊗b)) <~~~> (bin_second b >>>> bin_second a).
- intros.
- set (fun c:C => mon_assoc (pair_obj (pair_obj a b) c)) as qq.
- simpl in qq.
- set (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (Fobj (pair_obj a b) ⋊-) (b ⋊- >>>> a ⋊-)) as qqq.
- set (qqq qq) as q'.
- apply q'.
- clear q'.
- clear qqq.
- abstract (intros; set ((ni_commutes mon_assoc) (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
- (pair_mor (pair_obj (pair_obj _ _) _) (pair_obj (pair_obj _ _) _)
- (pair_mor (pair_obj _ _) (pair_obj _ _) (id a) (id b)) f)) as qr;
- etransitivity; [ apply qr | idtac ];
- apply comp_respects; try reflexivity;
- unfold mon_f;
- simpl;
- apply ((fmor_respects F) (pair_obj _ _) (pair_obj _ _));
- split; try reflexivity;
- simpl;
- set (@fmor_preserves_id _ _ _ _ _ _ _ F (pair_obj a b)) as qqqq;
- simpl in qqqq;
- apply qqqq).
- Defined.
+(* we can go the other way: given a monoidal category, its left/right functors can be combined into a bifunctor *)
+Section Bifunctor_from_MonoidalCat.
+ Context `(M:MonoidalCat).
- Lemma mon_pmon_cancelr : (bin_first I0) <~~~> functor_id C.
- set (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (bin_first I0) (functor_id C)) as qq.
- set (mon_cancelr) as z.
- simpl in z.
- simpl in qq.
- set (qq z) as zz.
- apply zz.
- abstract (intros;
- set (ni_commutes mon_cancelr) as q; simpl in *;
- apply q).
- Defined.
- Lemma mon_pmon_cancell : (bin_second I0) <~~~> functor_id C.
- set (@Build_NaturalIsomorphism _ _ _ _ _ _ _ _ (bin_second I0) (functor_id C)) as qq.
- set (mon_cancell) as z.
- simpl in z.
- simpl in qq.
- set (qq z) as zz.
- apply zz.
- abstract (intros;
- set (ni_commutes mon_cancell) as q; simpl in *;
- apply q).
+ Definition Bifunctor_from_MonoidalCat_fobj : M ×× M -> M.
+ intro x.
+ destruct x.
+ exact (bin_obj' o o0).
Defined.
- Lemma mon_pmon_triangle : forall a b, #(mon_pmon_cancelr a) ⋉ b ~~ #(mon_pmon_assoc _ _ _) >>> a ⋊ #(mon_pmon_cancell b).
- intros.
- set mon_triangle as q.
- simpl in q.
- apply q.
- Qed.
-
- Lemma mon_pmon_pentagon a b c d : (#(mon_pmon_assoc a c b ) ⋉ d) >>>
- #(mon_pmon_assoc a d _ ) >>>
- (a ⋊ #(mon_pmon_assoc b d c))
- ~~ #(mon_pmon_assoc _ d c ) >>>
- #(mon_pmon_assoc a _ b ).
- set (@pentagon _ _ _ _ _ _ _ mon_pentagon) as x.
- simpl in x.
- unfold bin_obj.
- unfold mon_first in x.
+ Definition Bifunctor_from_MonoidalCat_fmor {a}{b}(f:a~~{M××M}~~>b)
+ : (Bifunctor_from_MonoidalCat_fobj a)~~{M}~~>(Bifunctor_from_MonoidalCat_fobj b).
+ destruct a; destruct b; destruct f.
simpl in *.
- apply x.
- Qed.
-
- Definition MonoidalCat_is_PreMonoidal : PreMonoidalCat (BinoidalCat_from_Bifunctor (mon_f M)) (mon_i M).
- refine {| pmon_assoc := mon_pmon_assoc
- ; pmon_cancell := mon_pmon_cancell
- ; pmon_cancelr := mon_pmon_cancelr
- ; pmon_triangle := {| triangle := mon_pmon_triangle |}
- ; pmon_pentagon := {| pentagon := mon_pmon_pentagon |}
- ; pmon_assoc_ll := mon_pmon_assoc_ll
- ; pmon_assoc_rr := mon_pmon_assoc_rr
- |}.
- abstract (set (coincide mon_triangle) as qq; simpl in *; apply qq).
- abstract (intros; simpl; reflexivity).
- abstract (intros; simpl; reflexivity).
+ apply (h ⋉ _ >>> _ ⋊ h0).
Defined.
- Lemma MonoidalCat_all_central : forall a b (f:a~~{M}~~>b), CentralMorphism f.
- intros;
- set (@fmor_preserves_comp _ _ _ _ _ _ _ M) as fc.
- apply Build_CentralMorphism;
- intros; simpl in *.
- etransitivity.
- apply fc.
- symmetry.
- etransitivity.
- apply fc.
- apply (fmor_respects M).
- simpl.
- setoid_rewrite left_identity;
- setoid_rewrite right_identity;
- split; reflexivity.
- etransitivity.
- apply fc.
- symmetry.
- etransitivity.
- apply fc.
- apply (fmor_respects M).
- simpl.
- setoid_rewrite left_identity;
- setoid_rewrite right_identity;
- split; reflexivity.
- Qed.
-
-End MonoidalCat_is_PreMonoidal.
-
-Hint Extern 1 => apply MonoidalCat_all_central.
-Coercion MonoidalCat_is_PreMonoidal : MonoidalCat >-> PreMonoidalCat.
-
-(* Later: generalize to premonoidal categories *)
-Class DiagonalCat `(mc:MonoidalCat(F:=F)) :=
-{ copy_nt : forall a, functor_id _ ~~~> func_diagonal >>>> F
-; copy : forall (a:mc), a~~{mc}~~>(bin_obj(BinoidalCat:=mc) a a)
- := fun a => nt_component _ _ (copy_nt a) a
+ Instance Bifunctor_from_MonoidalCat : Functor (M ×× M) M Bifunctor_from_MonoidalCat_fobj :=
+ { fmor := fun x y f => Bifunctor_from_MonoidalCat_fmor f }.
+ intros; simpl.
+ destruct a; destruct b; destruct f; destruct f'; simpl in *.
+ destruct H.
+ apply comp_respects.
+ apply (fmor_respects (-⋉o0)); auto.
+ apply (fmor_respects (o1⋊-)); auto.
+ intros; destruct a; simpl in *.
+ setoid_rewrite (fmor_preserves_id (-⋉o0)).
+ setoid_rewrite left_identity.
+ apply fmor_preserves_id.
+ intros; destruct a; destruct b; destruct c; destruct f; destruct g; simpl in *.
+ setoid_rewrite <- fmor_preserves_comp.
+ setoid_rewrite juggle3 at 1.
+ assert (CentralMorphism h1).
+ apply mon_commutative.
+ setoid_rewrite <- (centralmor_first(CentralMorphism:=H)).
+ setoid_rewrite <- juggle3.
+ reflexivity.
+ Defined.
+
+End Bifunctor_from_MonoidalCat.
+
+
+Class DiagonalCat `(mc:MonoidalCat) :=
+{ copy : forall (a:mc), a~~{mc}~~>(bin_obj(BinoidalCat:=mc) a a)
+; copy_natural1 : forall {a}{b}(f:a~~{mc}~~>b)(c:mc), copy _ >>> f ⋉ a >>> b ⋊ f ~~ f >>> copy _
+; copy_natural2 : forall {a}{b}(f:a~~{mc}~~>b)(c:mc), copy _ >>> a ⋊ f >>> f ⋉ b ~~ f >>> copy _
(* for non-cartesian braided diagonal categories we also need: copy >> swap == copy *)
}.
Class CartesianCat `(mc:MonoidalCat) :=
-{ car_terminal : Terminal mc
-; car_one : (@one _ _ _ car_terminal) ≅ (mon_i mc)
-; car_diagonal : DiagonalCat mc
-; car_law1 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> ((drop a >>> #car_one) ⋉ a) >>> (#(pmon_cancell mc _))
-; car_law2 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (a ⋊ (drop a >>> #car_one)) >>> (#(pmon_cancelr mc _))
+{ car_terminal :> Terminal mc
+; car_one : one ≅ pmon_I
+; car_diagonal : DiagonalCat mc
+; car_law1 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> ((drop a >>> #car_one) ⋉ a) >>> (#(pmon_cancell _))
+; car_law2 : forall {a}, id a ~~ (copy(DiagonalCat:=car_diagonal) a) >>> (a ⋊ (drop a >>> #car_one)) >>> (#(pmon_cancelr _))
; car_mn := mc
}.
Coercion car_diagonal : CartesianCat >-> DiagonalCat.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
-Require Import ProductCategories_ch1_6_1.
(*******************************************************************************)
(* Chapter 7.5: Natural Isomorphisms *)
Defined.
Section ni_prod_comp.
+Require Import ProductCategories_ch1_6_1.
Context
`{C1:Category}`{C2:Category}
`{D1:Category}`{D2:Category}
Defined.
End ni_prod_comp.
-Structure Retraction `{C:Category} `{D:Category} :=
-{ retraction_section_fobj : C -> D
-; retraction_section : Functor C D retraction_section_fobj
-; retraction_retraction_fobj : D -> C
-; retraction_retraction : Functor D C retraction_retraction_fobj
-; retraction_composes : retraction_section >>>> retraction_retraction ≃ functor_id _
-}.
-Implicit Arguments Retraction [ [Ob] [Hom] [Ob0] [Hom0] ].
-Coercion retraction_section : Retraction >-> Functor.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
-Require Import ProductCategories_ch1_6_1.
Require Import InitialTerminal_ch2_2.
Require Import Subcategories_ch7_1.
Require Import NaturalTransformations_ch7_4.
(* not in Awodey *)
Class PreMonoidalCat `(bc:BinoidalCat(C:=C))(I:C) :=
-{ pmon_I := I
-; pmon_bin := bc
-; pmon_cat := C
-; pmon_assoc : forall a b, (bin_second a >>>> bin_first b) <~~~> (bin_first b >>>> bin_second a)
-; pmon_cancelr : (bin_first I) <~~~> functor_id C
-; pmon_cancell : (bin_second I) <~~~> functor_id C
-; pmon_pentagon : Pentagon (fun a b c f => f ⋉ c) (fun a b c f => c ⋊ f) (fun a b c => #((pmon_assoc a c) b))
-; pmon_triangle : Triangle (fun a b c f => f ⋉ c) (fun a b c f => c ⋊ f) (fun a b c => #((pmon_assoc a c) b))
- (fun a => #(pmon_cancell a)) (fun a => #(pmon_cancelr a))
-; pmon_assoc_rr : forall a b, (bin_first (a⊗b)) <~~~> (bin_first a >>>> bin_first b)
-; pmon_assoc_ll : forall a b, (bin_second (a⊗b)) <~~~> (bin_second b >>>> bin_second a)
-; pmon_coherent_r : forall a c d:C, #(pmon_assoc_rr c d a) ~~ #(pmon_assoc a d c)⁻¹
-; pmon_coherent_l : forall a c d:C, #(pmon_assoc_ll c a d) ~~ #(pmon_assoc c d a)
+{ pmon_I := I
+; pmon_bin := bc
+; pmon_cat := C
+; pmon_assoc : forall a b, (bin_second a >>>> bin_first b) <~~~> (bin_first b >>>> bin_second a)
+; pmon_cancelr : (bin_first I) <~~~> functor_id C
+; pmon_cancell : (bin_second I) <~~~> functor_id C
+; pmon_pentagon : Pentagon (fun a b c f => f ⋉ c) (fun a b c f => c ⋊ f) (fun a b c => #((pmon_assoc a c) b))
+; pmon_triangle : Triangle (fun a b c f => f ⋉ c) (fun a b c f => c ⋊ f) (fun a b c => #((pmon_assoc a c) b))
+ (fun a => #(pmon_cancell a)) (fun a => #(pmon_cancelr a))
+; pmon_assoc_rr : forall a b, (bin_first (a⊗b)) <~~~> (bin_first a >>>> bin_first b)
+; pmon_assoc_ll : forall a b, (bin_second (a⊗b)) <~~~> (bin_second b >>>> bin_second a)
+; pmon_coherent_r : forall a c d:C, #(pmon_assoc_rr c d a) ~~ #(pmon_assoc a d c)⁻¹
+; pmon_coherent_l : forall a c d:C, #(pmon_assoc_ll c a d) ~~ #(pmon_assoc c d a)
+; pmon_assoc_central : forall a b c, CentralMorphism #(pmon_assoc a b c)
+; pmon_cancelr_central : forall a , CentralMorphism #(pmon_cancelr a)
+; pmon_cancell_central : forall a , CentralMorphism #(pmon_cancell a)
}.
(*
* Premonoidal categories actually have three associators (the "f"
* might need extra versions of the triangle/pentagon diagrams.
*)
-Implicit Arguments pmon_cancell [ Ob Hom C bin_obj' bc I ].
-Implicit Arguments pmon_cancelr [ Ob Hom C bin_obj' bc I ].
-Implicit Arguments pmon_assoc [ Ob Hom C bin_obj' bc I ].
+Implicit Arguments pmon_cancell [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
+Implicit Arguments pmon_cancelr [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
+Implicit Arguments pmon_assoc [ Ob Hom C bin_obj' bc I PreMonoidalCat ].
Coercion pmon_bin : PreMonoidalCat >-> BinoidalCat.
(* this turns out to be Exercise VII.1.1 from Mac Lane's CWM *)
Lemma MacLane_ex_VII_1_1 `{mn:PreMonoidalCat(I:=EI)} a b
- : #((pmon_cancelr mn) (a ⊗ b)) ~~ #((pmon_assoc mn a EI) b) >>> (a ⋊-) \ #((pmon_cancelr mn) b).
+ : #(pmon_cancelr (a ⊗ b)) ~~ #((pmon_assoc a EI) b) >>> (a ⋊-) \ #(pmon_cancelr b).
set (pmon_pentagon EI EI a b) as penta. unfold pmon_pentagon in penta.
set (pmon_triangle a b) as tria. unfold pmon_triangle in tria.
apply (fmor_respects(bin_second EI)) in tria.
set (@fmor_preserves_comp) as fpc.
setoid_rewrite <- fpc in tria.
- set (ni_commutes (pmon_assoc mn a b)) as xx.
+ set (ni_commutes (pmon_assoc a b)) as xx.
(* FIXME *)
Admitted.
`(PM1:PreMonoidalCat(C:=C1)(I:=I1))
`(PM2:PreMonoidalCat(C:=C2)(I:=I2))
(fobj : C1 -> C2 ) :=
-{ mf_F :> Functor C1 C2 fobj
-; mf_preserves_i : mf_F I1 ≅ I2
-; mf_preserves_first : forall a, bin_first a >>>> mf_F <~~~> mf_F >>>> bin_first (mf_F a)
-; mf_preserves_second : forall a, bin_second a >>>> mf_F <~~~> mf_F >>>> bin_second (mf_F a)
-; mf_preserves_center : forall `(f:a~>b), CentralMorphism f -> CentralMorphism (mf_F \ f)
+{ mf_F :> Functor C1 C2 fobj
+; mf_i : I2 ≅ mf_F I1
+; mf_first : ∀ a, mf_F >>>> bin_first (mf_F a) <~~~> bin_first a >>>> mf_F
+; mf_second : ∀ a, mf_F >>>> bin_second (mf_F a) <~~~> bin_second a >>>> mf_F
+; mf_consistent : ∀ a b, #(mf_first a b) ~~ #(mf_second b a)
+; mf_center : forall `(f:a~>b), CentralMorphism f -> CentralMorphism (mf_F \ f)
+; mf_cancell : ∀ b, #(pmon_cancell _) ~~ #mf_i ⋉ _ >>> #(mf_first b I1) >>> mf_F \ #(pmon_cancell b)
+; mf_cancelr : ∀ a, #(pmon_cancelr _) ~~ _ ⋊ #mf_i >>> #(mf_second a I1) >>> mf_F \ #(pmon_cancelr a)
+; mf_assoc : ∀ a b c, #(pmon_assoc _ _ _) >>> _ ⋊ #(mf_second _ _) >>> #(mf_second _ _) ~~
+ #(mf_second _ _) ⋉ _ >>> #(mf_second _ _) >>> mf_F \ #(pmon_assoc a c b)
}.
Coercion mf_F : PreMonoidalFunctor >-> Functor.
+Definition PreMonoidalFunctorsCompose
+ `{PM1 :PreMonoidalCat(C:=C1)(I:=I1)}
+ `{PM2 :PreMonoidalCat(C:=C2)(I:=I2)}
+ {fobj12:C1 -> C2 }
+ (PMF12 :PreMonoidalFunctor PM1 PM2 fobj12)
+ `{PM3 :PreMonoidalCat(C:=C3)(I:=I3)}
+ {fobj23:C2 -> C3 }
+ (PMF23 :PreMonoidalFunctor PM2 PM3 fobj23)
+ : PreMonoidalFunctor PM1 PM3 (fobj23 ○ fobj12).
+ admit.
+ Defined.
+
(*******************************************************************************)
(* Braided and Symmetric Categories *)
Class BraidedCat `(mc:PreMonoidalCat) :=
{ br_niso : forall a, bin_first a <~~~> bin_second a
; br_swap := fun a b => ni_iso (br_niso b) a
-; triangleb : forall a:C, #(pmon_cancelr mc a) ~~ #(br_swap a (pmon_I(PreMonoidalCat:=mc))) >>> #(pmon_cancell mc a)
-; hexagon1 : forall {a b c}, #(pmon_assoc mc _ _ _) >>> #(br_swap a _) >>> #(pmon_assoc mc _ _ _)
- ~~ #(br_swap _ _) ⋉ c >>> #(pmon_assoc mc _ _ _) >>> b ⋊ #(br_swap _ _)
-; hexagon2 : forall {a b c}, #(pmon_assoc mc _ _ _)⁻¹ >>> #(br_swap _ c) >>> #(pmon_assoc mc _ _ _)⁻¹
- ~~ a ⋊ #(br_swap _ _) >>> #(pmon_assoc mc _ _ _)⁻¹ >>> #(br_swap _ _) ⋉ b
+; triangleb : forall a:C, #(pmon_cancelr a) ~~ #(br_swap a (pmon_I(PreMonoidalCat:=mc))) >>> #(pmon_cancell a)
+; hexagon1 : forall {a b c}, #(pmon_assoc _ _ _) >>> #(br_swap a _) >>> #(pmon_assoc _ _ _)
+ ~~ #(br_swap _ _) ⋉ c >>> #(pmon_assoc _ _ _) >>> b ⋊ #(br_swap _ _)
+; hexagon2 : forall {a b c}, #(pmon_assoc _ _ _)⁻¹ >>> #(br_swap _ c) >>> #(pmon_assoc _ _ _)⁻¹
+ ~~ a ⋊ #(br_swap _ _) >>> #(pmon_assoc _ _ _)⁻¹ >>> #(br_swap _ _) ⋉ b
}.
Class SymmetricCat `(bc:BraidedCat) :=
{ symcat_swap : forall a b:C, #((br_swap(BraidedCat:=bc)) a b) ~~ #(br_swap _ _)⁻¹
}.
+
+
+Section PreMonoidalSubCategory.
+
+ Context `(pm:PreMonoidalCat(I:=pmI)).
+ Context {Pobj}{Pmor}(S:SubCategory pm Pobj Pmor).
+ Context (Pobj_unit:Pobj pmI).
+ Context (Pobj_closed:forall {a}{b}, Pobj a -> Pobj b -> Pobj (a⊗b)).
+ Implicit Arguments Pobj_closed [[a][b]].
+ Context (Pmor_first: forall {a}{b}{c}{f}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c)(pf:Pmor _ _ pa pb f),
+ Pmor _ _ (Pobj_closed pa pc) (Pobj_closed pb pc) (f ⋉ c)).
+ Context (Pmor_second: forall {a}{b}{c}{f}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c)(pf:Pmor _ _ pa pb f),
+ Pmor _ _ (Pobj_closed pc pa) (Pobj_closed pc pb) (c ⋊ f)).
+ Context (Pmor_assoc: forall {a}{b}{c}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c),
+ Pmor _ _
+ (Pobj_closed (Pobj_closed pa pb) pc)
+ (Pobj_closed pa (Pobj_closed pb pc))
+ #(pmon_assoc a c b)).
+ Context (Pmor_unassoc: forall {a}{b}{c}(pa:Pobj a)(pb:Pobj b)(pc:Pobj c),
+ Pmor _ _
+ (Pobj_closed pa (Pobj_closed pb pc))
+ (Pobj_closed (Pobj_closed pa pb) pc)
+ #(pmon_assoc a c b)⁻¹).
+ Context (Pmor_cancell: forall {a}(pa:Pobj a),
+ Pmor _ _ (Pobj_closed Pobj_unit pa) pa
+ #(pmon_cancell a)).
+ Context (Pmor_uncancell: forall {a}(pa:Pobj a),
+ Pmor _ _ pa (Pobj_closed Pobj_unit pa)
+ #(pmon_cancell a)⁻¹).
+ Context (Pmor_cancelr: forall {a}(pa:Pobj a),
+ Pmor _ _ (Pobj_closed pa Pobj_unit) pa
+ #(pmon_cancelr a)).
+ Context (Pmor_uncancelr: forall {a}(pa:Pobj a),
+ Pmor _ _ pa (Pobj_closed pa Pobj_unit)
+ #(pmon_cancelr a)⁻¹).
+ Implicit Arguments Pmor_first [[a][b][c][f]].
+ Implicit Arguments Pmor_second [[a][b][c][f]].
+
+ Definition PreMonoidalSubCategory_bobj (x y:S) :=
+ existT Pobj _ (Pobj_closed (projT2 x) (projT2 y)).
+
+ Definition PreMonoidalSubCategory_first_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
+ (PreMonoidalSubCategory_bobj x a)~~{S}~~>(PreMonoidalSubCategory_bobj y a).
+ unfold hom; simpl; intros.
+ destruct f.
+ destruct a as [a apf].
+ destruct x as [x xpf].
+ destruct y as [y ypf].
+ simpl in *.
+ exists (x0 ⋉ a).
+ apply Pmor_first; auto.
+ Defined.
+
+ Definition PreMonoidalSubCategory_second_fmor (a:S) : forall {x}{y}(f:x~~{S}~~>y),
+ (PreMonoidalSubCategory_bobj a x)~~{S}~~>(PreMonoidalSubCategory_bobj a y).
+ unfold hom; simpl; intros.
+ destruct f.
+ destruct a as [a apf].
+ destruct x as [x xpf].
+ destruct y as [y ypf].
+ simpl in *.
+ exists (a ⋊ x0).
+ apply Pmor_second; auto.
+ Defined.
+
+ Instance PreMonoidalSubCategory_first (a:S)
+ : Functor (S) (S) (fun x => PreMonoidalSubCategory_bobj x a) :=
+ { fmor := fun x y f => PreMonoidalSubCategory_first_fmor a f }.
+ unfold PreMonoidalSubCategory_first_fmor; intros; destruct a; destruct a0; destruct b; destruct f; destruct f'; simpl in *.
+ apply (fmor_respects (-⋉x)); auto.
+ unfold PreMonoidalSubCategory_first_fmor; intros; destruct a; destruct a0; simpl in *.
+ apply (fmor_preserves_id (-⋉x)); auto.
+ unfold PreMonoidalSubCategory_first_fmor; intros;
+ destruct a; destruct a0; destruct b; destruct c; destruct f; destruct g; simpl in *.
+ apply (fmor_preserves_comp (-⋉x)); auto.
+ Defined.
+
+ Instance PreMonoidalSubCategory_second (a:S)
+ : Functor (S) (S) (fun x => PreMonoidalSubCategory_bobj a x) :=
+ { fmor := fun x y f => PreMonoidalSubCategory_second_fmor a f }.
+ unfold PreMonoidalSubCategory_second_fmor; intros; destruct a; destruct a0; destruct b; destruct f; destruct f'; simpl in *.
+ apply (fmor_respects (x⋊-)); auto.
+ unfold PreMonoidalSubCategory_second_fmor; intros; destruct a; destruct a0; simpl in *.
+ apply (fmor_preserves_id (x⋊-)); auto.
+ unfold PreMonoidalSubCategory_second_fmor; intros;
+ destruct a; destruct a0; destruct b; destruct c; destruct f; destruct g; simpl in *.
+ apply (fmor_preserves_comp (x⋊-)); auto.
+ Defined.
+
+ Instance PreMonoidalSubCategory_is_Binoidal : BinoidalCat S PreMonoidalSubCategory_bobj :=
+ { bin_first := PreMonoidalSubCategory_first
+ ; bin_second := PreMonoidalSubCategory_second }.
+
+ Definition PreMonoidalSubCategory_assoc
+ : forall a b,
+ (PreMonoidalSubCategory_second a >>>> PreMonoidalSubCategory_first b) <~~~>
+ (PreMonoidalSubCategory_first b >>>> PreMonoidalSubCategory_second a).
+ admit.
+ Defined.
+
+ Definition PreMonoidalSubCategory_assoc_ll
+ : forall a b,
+ PreMonoidalSubCategory_second (a⊗b) <~~~>
+ PreMonoidalSubCategory_second b >>>> PreMonoidalSubCategory_second a.
+ intros.
+ admit.
+ Defined.
+
+ Definition PreMonoidalSubCategory_assoc_rr
+ : forall a b,
+ PreMonoidalSubCategory_first (a⊗b) <~~~>
+ PreMonoidalSubCategory_first a >>>> PreMonoidalSubCategory_first b.
+ intros.
+ admit.
+ Defined.
+
+ Definition PreMonoidalSubCategory_I := existT _ pmI (Pobj_unit).
+
+ Definition PreMonoidalSubCategory_cancelr : PreMonoidalSubCategory_first PreMonoidalSubCategory_I <~~~> functor_id _.
+ admit.
+ Defined.
+
+ Definition PreMonoidalSubCategory_cancell : PreMonoidalSubCategory_second PreMonoidalSubCategory_I <~~~> functor_id _.
+ admit.
+ Defined.
+
+ Instance PreMonoidalSubCategory_PreMonoidal : PreMonoidalCat PreMonoidalSubCategory_is_Binoidal PreMonoidalSubCategory_I :=
+ { pmon_assoc := PreMonoidalSubCategory_assoc
+ ; pmon_assoc_rr := PreMonoidalSubCategory_assoc_rr
+ ; pmon_assoc_ll := PreMonoidalSubCategory_assoc_ll
+ ; pmon_cancelr := PreMonoidalSubCategory_cancelr
+ ; pmon_cancell := PreMonoidalSubCategory_cancell
+ }.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ admit.
+ Defined.
+
+End PreMonoidalSubCategory.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
-Require Import ProductCategories_ch1_6_1.
Require Import InitialTerminal_ch2_2.
Require Import Subcategories_ch7_1.
Require Import NaturalTransformations_ch7_4.
Require Import Coherence_ch7_8.
Require Import BinoidalCategories.
Require Import PreMonoidalCategories.
-Require Import MonoidalCategories_ch_7_8.
+Require Import MonoidalCategories_ch7_8.
(******************************************************************************)
(* Facts about the center of a Binoidal or PreMonoidal Category *)
setoid_rewrite pmon_coherent_l at 1.
setoid_rewrite juggle3.
setoid_rewrite juggle3.
- set (@iso_comp2 _ _ _ _ _ ((pmon_assoc C b c0) c)) as q.
+ set (@iso_comp2 _ _ _ _ _ ((pmon_assoc b c0) c)) as q.
setoid_rewrite q.
clear q.
setoid_rewrite right_identity.
setoid_rewrite q.
clear q.
- set (ni_commutes (pmon_assoc _ d c) f) as q.
+ set (ni_commutes (pmon_assoc d c) f) as q.
apply iso_shift_right' in q.
unfold fmor in q at 1; simpl in q.
rewrite q.
clear q.
setoid_rewrite juggle3.
- setoid_rewrite (iso_comp1 ((pmon_assoc C d c) a)).
+ set (iso_comp1 ((pmon_assoc d c) a)) as q.
+ setoid_rewrite q.
+ clear q.
setoid_rewrite right_identity.
set (ni_commutes (pmon_assoc_rr b c) g) as q.
setoid_rewrite q.
clear q.
- set (ni_commutes (pmon_assoc _ c0 c) f) as q.
+ set (ni_commutes (pmon_assoc c0 c) f) as q.
unfold fmor in q; simpl in q.
apply iso_shift_right' in q.
rewrite q.
setoid_rewrite juggle3.
setoid_rewrite juggle3.
- setoid_rewrite (iso_comp1 ((pmon_assoc C c0 c) b)).
+ set (iso_comp1 ((pmon_assoc c0 c) b)) as q.
+ setoid_rewrite q.
+ clear q.
setoid_rewrite right_identity.
setoid_rewrite pmon_coherent_r.
setoid_rewrite q.
clear q.
- set (ni_commutes (pmon_assoc _ c d) f) as q.
+ set (ni_commutes (pmon_assoc c d) f) as q.
apply symmetry in q.
apply iso_shift_left' in q.
unfold fmor in q at 1; simpl in q.
setoid_rewrite q.
clear q.
- set (ni_commutes (pmon_assoc _ c c0) f) as q.
+ set (ni_commutes (pmon_assoc c c0) f) as q.
unfold fmor in q; simpl in q.
symmetry in q.
apply iso_shift_left' in q.
rewrite pmon_coherent_l.
setoid_rewrite <- associativity.
setoid_rewrite juggle3.
- set (iso_comp2 ((pmon_assoc _ c c0) b)) as q.
+ set (iso_comp2 ((pmon_assoc c c0) b)) as q.
setoid_rewrite q.
setoid_rewrite right_identity.
clear q.
setoid_rewrite <- associativity.
setoid_rewrite juggle3.
setoid_rewrite pmon_coherent_r.
- set (iso_comp1 ((pmon_assoc C c0 b) c)) as x.
+ set (iso_comp1 ((pmon_assoc c0 b) c)) as x.
setoid_rewrite x.
clear x.
setoid_rewrite right_identity.
reflexivity.
Qed.
-Section CenterMonoidal.
+Section Center_is_Monoidal.
- Context `(mc:PreMonoidalCat(I:=pI)).
+ Context `(pm:PreMonoidalCat(I:=pmI)).
- Definition CenterMonoidal_Fobj : (Center mc) ×× (Center mc) -> Center mc.
- intro.
- destruct X as [a b].
- destruct a as [a apf].
- destruct b as [b bpf].
- exists (a ⊗ b); auto.
+ Definition Center_bobj : Center pm -> Center pm -> Center pm.
+ apply PreMonoidalSubCategory_bobj.
+ intros; auto.
Defined.
- Definition CenterMonoidal_F_fmor (a b:(Center mc) ×× (Center mc)) :
- (a~~{(Center mc) ×× (Center mc)}~~>b) ->
- ((CenterMonoidal_Fobj a)~~{Center mc}~~>(CenterMonoidal_Fobj b)).
- destruct a as [[a1 a1'] [a2 a2']].
- destruct b as [[b1 b1'] [b2 b2']].
- intro f.
- destruct f as [[f1 f1'] [f2 f2']].
- simpl in *.
- unfold hom.
- simpl.
- exists (f1 ⋉ a2 >>> b1 ⋊ f2).
- apply central_morphisms_compose.
- apply first_preserves_centrality; auto.
- apply second_preserves_centrality; auto.
- Defined.
-
- Definition CenterMonoidal_F : Functor _ _ CenterMonoidal_Fobj.
- refine {| fmor := CenterMonoidal_F_fmor |}.
- intros.
- destruct a as [[a1 a1'] [a2 a2']].
- destruct b as [[b1 b1'] [b2 b2']].
- destruct f as [[f1 f1'] [f2 f2']].
- destruct f' as [[g1 g1'] [g2 g2']].
- simpl in *.
- destruct H.
- apply comp_respects.
- set (fmor_respects(-⋉a2)) as q; apply q; auto.
- set (fmor_respects(b1⋊-)) as q; apply q; auto.
+ Definition Center_is_Binoidal : BinoidalCat (Center pm) Center_bobj.
+ apply PreMonoidalSubCategory_is_Binoidal.
intros.
- destruct a as [[a1 a1'] [a2 a2']].
- simpl in *.
- setoid_rewrite (fmor_preserves_id (-⋉a2)).
- setoid_rewrite (fmor_preserves_id (a1⋊-)).
- apply left_identity.
+ apply first_preserves_centrality; auto.
intros.
- destruct a as [[a1 a1'] [a2 a2']].
- destruct b as [[b1 b1'] [b2 b2']].
- destruct c as [[c1 c1'] [c2 c2']].
- destruct f as [[f1 f1'] [f2 f2']].
- destruct g as [[g1 g1'] [g2 g2']].
- simpl in *.
- setoid_rewrite juggle3.
- setoid_rewrite <- (centralmor_first(CentralMorphism:=g1')).
- setoid_rewrite <- juggle3.
- setoid_rewrite <- fmor_preserves_comp.
- reflexivity.
- Defined.
-
- Definition center_I : Center mc := exist _ pI I.
-
- Definition center_cancelr : (func_rlecnac center_I >>>> CenterMonoidal_F) <~~~> functor_id (Center mc).
- Definition center_cancelr_niso : ∀A : Center mc, CenterMonoidal_Fobj (pair_obj A center_I) ≅ A.
- intros.
- destruct A; simpl.
- set (ni_iso (pmon_cancelr mc) x) as q.
- (*refine {| iso_forward := #q ; iso_backward := iso_backward q |}.*)
- admit.
- Defined.
- refine {| ni_iso := center_cancelr_niso |}.
- admit.
- Defined.
-
- Definition center_cancell : (func_llecnac center_I >>>> CenterMonoidal_F) <~~~> functor_id (Center mc).
- Definition center_cancell_niso : ∀A : Center mc, CenterMonoidal_Fobj (pair_obj center_I A) ≅ A.
- admit.
- Defined.
- refine {| ni_iso := center_cancell_niso |}.
- admit.
+ apply second_preserves_centrality; auto.
Defined.
- Definition center_assoc :
- ((CenterMonoidal_F **** (functor_id _)) >>>> CenterMonoidal_F)
- <~~~> func_cossa >>>> ((((functor_id _) **** CenterMonoidal_F) >>>> CenterMonoidal_F)).
-
- Definition center_assoc_niso : ∀A : (Center mc ×× Center mc) ×× Center mc,
- ((((CenterMonoidal_F **** (functor_id _)) >>>> CenterMonoidal_F) A))
- ≅ ((func_cossa >>>> ((((functor_id _) **** CenterMonoidal_F) >>>> CenterMonoidal_F))) A).
- admit.
- Defined.
-
- refine {| ni_iso := center_assoc_niso |}.
- admit.
+ Definition Center_is_PreMonoidal : PreMonoidalCat Center_is_Binoidal (exist _ pmI I).
+ apply PreMonoidalSubCategory_PreMonoidal.
Defined.
- Instance CenterMonoidal : MonoidalCat _ _ CenterMonoidal_F (exist _ pI I) :=
- { mon_cancelr := center_cancelr
- ; mon_cancell := center_cancell
- ; mon_assoc := center_assoc
- }.
- admit.
- admit.
+ Definition Center_is_Monoidal : MonoidalCat Center_is_PreMonoidal.
+ apply Build_MonoidalCat.
+ apply Build_CommutativeCat.
+ intros.
+ apply Build_CentralMorphism; unfold hom;
+ intros; destruct f; destruct a; destruct c; destruct d; destruct b; destruct g; simpl in *.
+ apply centralmor_second.
+ apply centralmor_second.
Defined.
-End CenterMonoidal.
+End Center_is_Monoidal.
Section RepresentableStructure.
Context `(ec:ECategory(mn:=mn)(V:=V)).
- Definition hom_contravariant {a:ec}{d e:ec}(f:EI~~{V}~~>(d~~>e)) := #(pmon_cancell mn _)⁻¹ >>> (f ⋉ (_ ~~> a)) >>> ecomp.
- Definition hom_covariant {a:ec}{d e:ec}(f:EI~~{V}~~>(d~~>e)) := #(pmon_cancelr mn _)⁻¹ >>> ((a ~~> d) ⋊ f) >>> ecomp.
+ Definition hom_contravariant {a:ec}{d e:ec}(f:EI~~{V}~~>(d~~>e)) := #(pmon_cancell _)⁻¹ >>> (f ⋉ (_ ~~> a)) >>> ecomp.
+ Definition hom_covariant {a:ec}{d e:ec}(f:EI~~{V}~~>(d~~>e)) := #(pmon_cancelr _)⁻¹ >>> ((a ~~> d) ⋊ f) >>> ecomp.
Lemma hom_covariant_distributes {a b c:ec}{x}(f:a~~{ec}~~>b)(g:b~~{ec}~~>c)
: hom_covariant (f >>> g) ~~ (hom_covariant (a:=x) f) >>> (hom_covariant g).
apply fmor_respects; auto.
intros.
unfold hom_covariant.
- apply (epic _ (iso_epic ((pmon_cancelr mn) (X ~~> a)))).
+ apply (epic _ (iso_epic ((pmon_cancelr) (X ~~> a)))).
setoid_rewrite <- associativity.
setoid_rewrite <- associativity.
setoid_rewrite iso_comp1.
End RepresentableStructure.
Opaque HomFunctor.
-Structure MonoidalEnrichment {e:Enrichment} :=
-{ me_enr :=e
-; me_fobj : prod_obj e e -> e
-; me_f : Functor (e ×× e) e me_fobj
-; me_i : e
-; me_mon : MonoidalCat e me_fobj me_f me_i
-; me_mf : MonoidalFunctor me_mon (enr_v_mon e) (HomFunctor e me_i)
-}.
-Implicit Arguments MonoidalEnrichment [ ].
-Coercion me_mon : MonoidalEnrichment >-> MonoidalCat.
-Coercion me_enr : MonoidalEnrichment >-> Enrichment.
-
-(* an enrichment for which hom(I,-) is monoidal, full, faithful, and conservative *)
-Structure MonicMonoidalEnrichment {e}{me:MonoidalEnrichment e} :=
-{ ffme_enr := me
-; ffme_mf_full : FullFunctor (HomFunctor e (me_i me))
-; ffme_mf_faithful : FaithfulFunctor (HomFunctor e (me_i me))
-; ffme_mf_conservative : ConservativeFunctor (HomFunctor e (me_i me))
-}.
-Implicit Arguments MonicMonoidalEnrichment [ ].
-Coercion ffme_enr : MonicMonoidalEnrichment >-> MonoidalEnrichment.
-Transparent HomFunctor.
-
-Structure SurjectiveMonicMonoidalEnrichment (e:Enrichment) :=
-{ smme_se : SurjectiveEnrichment e
-; smme_monoidal : MonoidalEnrichment e
-; smme_me : MonicMonoidalEnrichment _ smme_monoidal
-}.
-Coercion smme_se : SurjectiveMonicMonoidalEnrichment >-> SurjectiveEnrichment.
-Coercion smme_me : SurjectiveMonicMonoidalEnrichment >-> MonicMonoidalEnrichment.
-
-(* like SurjectiveMonicMonoidalEnrichment, but the Enrichment is a field, not a parameter *)
-Structure SMME :=
-{ smme_e : Enrichment
-; smme_see : SurjectiveEnrichment smme_e
-; smme_mon : MonoidalEnrichment smme_e
-; smme_mee : MonicMonoidalEnrichment _ smme_mon
-}.
-Coercion smme_e : SMME >-> Enrichment.
-Coercion smme_see : SMME >-> SurjectiveEnrichment.
-Coercion smme_mon : SMME >-> MonoidalEnrichment.
-Coercion smme_mee : SMME >-> MonicMonoidalEnrichment.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
Require Import ProductCategories_ch1_6_1.
+Require Import NaturalIsomorphisms_ch7_5.
(******************************************************************************)
(* Chapter 2.4: Sections and Retractions *)
}.
simpl; split; apply retract_pf.
Defined.
+
+Structure Retraction `{C:Category} `{D:Category} :=
+{ retraction_section_fobj : C -> D
+; retraction_section : Functor C D retraction_section_fobj
+; retraction_retraction_fobj : D -> C
+; retraction_retraction : Functor D C retraction_retraction_fobj
+; retraction_composes : retraction_section >>>> retraction_retraction ≃ functor_id _
+}.
+Implicit Arguments Retraction [ [Ob] [Hom] [Ob0] [Hom0] ].
+Coercion retraction_section : Retraction >-> Functor.
Qed.
End RestrictToImage.
-Instance func_opSubcat `(c1:Category Ob1 Hom1)`(c2:Category Ob Hom)`(SP:@SubCategory _ _ c2 Pobj Pmor)
+Instance func_opSubcat `(c1:Category)`(c2:Category)`(SP:@SubCategory _ _ c2 Pobj Pmor)
{fobj}(F:Functor c1⁽ºᑭ⁾ SP fobj) : Functor c1 SP⁽ºᑭ⁾ fobj :=
{ fmor := fun a b f => fmor F f }.
intros. apply (@fmor_respects _ _ _ _ _ _ _ F _ _ f f' H).
`{D:Category}
{Fobj}
(F:@Functor _ _ C _ _ D Fobj) := forall
- `{E:Category}
+ Eob EHom (E:@Category Eob EHom)
`{G :@Functor _ _ E _ _ C Gobj'}
`{H :@Functor _ _ E _ _ C Hobj'},
G >>>> F ≃ H >>>> F
projects / coq-categories.git / commitdiff