FreydCategories: add strictness requirement for unit object

[coq-categories.git] / src / FreydCategories.v

diff --git a/src/FreydCategories.v b/src/FreydCategories.v
index 7fe727d..8b921df 100644 (file)
--- a/src/FreydCategories.v
+++ b/src/FreydCategories.v
@@ -3,8 +3,7 @@
 (*******************************************************************************)
 
 Generalizable All Variables.
-Require Import Preamble.
-Require Import General.
+Require Import Notations.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.
@@ -14,33 +13,34 @@ Require Import Subcategories_ch7_1.
 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
-{ Ob                          :  Type                                   }
-{ freyd_bobj                  :  Ob -> Ob -> Ob                         }
-{ HomC                        :  Ob -> Ob -> Type                       }
-{ freyd_C                     :  Category Ob HomC                       }
-{ freyd_C_terminal            :  Terminal    freyd_C                    }
-{ freyd_C_binoidal            :  BinoidalCat freyd_C freyd_bobj         }
-( freyd_C_monoidal            :  PreMonoidalCat freyd_C_binoidal 1      )
-{ freyd_K_hom                 :  Ob -> Ob -> Type                       }
-( freyd_K                     :  Category Ob freyd_K_hom                )
-:=
-{ freyd_K_                    := freyd_K
-; freyd_C_cartesian           :  CartesianCat freyd_C_monoidal
-; freyd_K_binoidal            :> BinoidalCat  freyd_K freyd_bobj
-; freyd_K_monoidal            :> PreMonoidalCat  freyd_K_binoidal (one(Terminal:=freyd_C_terminal))
-; freyd_K_braided             :  BraidedCat   freyd_K_monoidal
-; freyd_K_symmetric           :  SymmetricCat freyd_K_braided
-; freyd_F                     :> PreMonoidalFunctor freyd_C_monoidal freyd_K_monoidal (fun x => x)
-; freyd_F_central             :  forall `(f:a~~{freyd_C}~~>b), CentralMorphism(C:=freyd_K) (freyd_F \ f)
-; freyd_F_strict_first        : forall a b,   #(mf_preserves_first(PreMonoidalFunctor:=freyd_F) a b) ~~ id (bin_first a b)
-; freyd_F_strict_second       : forall a b,   #(mf_preserves_second(PreMonoidalFunctor:=freyd_F) a b) ~~ id (bin_second a b)
-; freyd_F_strict_a            : forall a b c, freyd_F \ #(pmon_assoc freyd_C_monoidal a b c) ~~ #(pmon_assoc freyd_K_monoidal _ _ _)
-; freyd_F_strict_cl           :  forall a,     freyd_F \ #(pmon_cancell freyd_C_monoidal a) ~~ #(pmon_cancell freyd_K_monoidal _)
-; freyd_F_strict_cr           :  forall a,     freyd_F \ #(pmon_cancelr freyd_C_monoidal a) ~~ #(pmon_cancelr freyd_K_monoidal _)
-}.
-Coercion freyd_K_monoidal : FreydCategory >-> PreMonoidalCat.
-Coercion freyd_F          : FreydCategory >-> PreMonoidalFunctor.
-Coercion freyd_K_         : FreydCategory >-> Category.
+
+   (* a cartesian category C *)
+  `(C:CartesianCat(Ob:=Ob)(C:=C1)(bin_obj':=bobj))
+
+   (* 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:=pmon_I C))
+
+   (* an identity-on-objects functor J:C->Z(K) *)
+:= { fc_J       : Functor C (Center_is_Monoidal K) (fun x => x)
+
+   (* which is a monoidal functor *)
+   ; fc_mf_J    : MonoidalFunctor C (Center_is_Monoidal K) fc_J
+
+   (* and strict (meaning the functor's coherence maps are identities) *)
+   ; fc_strict_first   : forall a b, #(mf_first(PreMonoidalFunctor:=fc_mf_J) a b) ~~ id _  (* mf_consistent gives us mf_second *)
+   ; fc_strict_id      : #(mf_i(PreMonoidalFunctor:=fc_mf_J)) ~~ id _
+
+   ; fc_C       := C
+   ; fc_K       := K
+   }.
+
+Coercion fc_mf_J   : FreydCategory >-> MonoidalFunctor.
+Coercion fc_K      : FreydCategory >-> PreMonoidalCat.
+