1 (*******************************************************************************)
3 (*******************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
8 Require Import Categories_ch1_3.
9 Require Import Functors_ch1_4.
10 Require Import Isomorphisms_ch1_5.
11 Require Import ProductCategories_ch1_6_1.
12 Require Import InitialTerminal_ch2_2.
13 Require Import Subcategories_ch7_1.
14 Require Import NaturalTransformations_ch7_4.
15 Require Import NaturalIsomorphisms_ch7_5.
16 Require Import Coherence_ch7_8.
17 Require Import MonoidalCategories_ch7_8.
21 { freyd_bobj : Ob -> Ob -> Ob }
22 { HomC : Ob -> Ob -> Type }
23 { freyd_C : Category Ob HomC }
24 { freyd_C_terminal : Terminal freyd_C }
25 { freyd_C_binoidal : BinoidalCat freyd_C freyd_bobj }
26 ( freyd_C_monoidal : PreMonoidalCat freyd_C_binoidal 1 )
27 { freyd_K_hom : Ob -> Ob -> Type }
28 ( freyd_K : Category Ob freyd_K_hom )
31 ; freyd_C_cartesian : CartesianCat freyd_C_monoidal
32 ; freyd_K_binoidal :> BinoidalCat freyd_K freyd_bobj
33 ; freyd_K_monoidal :> PreMonoidalCat freyd_K_binoidal (one(Terminal:=freyd_C_terminal))
34 ; freyd_K_braided : BraidedCat freyd_K_monoidal
35 ; freyd_K_symmetric : SymmetricCat freyd_K_braided
36 ; freyd_F :> PreMonoidalFunctor freyd_C_monoidal freyd_K_monoidal (fun x => x)
37 ; freyd_F_central : forall `(f:a~~{freyd_C}~~>b), CentralMorphism(C:=freyd_K) (freyd_F \ f)
38 ; freyd_F_strict_first : forall a b, #(mf_preserves_first(PreMonoidalFunctor:=freyd_F) a b) ~~ id (bin_first a b)
39 ; freyd_F_strict_second : forall a b, #(mf_preserves_second(PreMonoidalFunctor:=freyd_F) a b) ~~ id (bin_second a b)
40 ; freyd_F_strict_a : forall a b c, freyd_F \ #(pmon_assoc freyd_C_monoidal a b c) ~~ #(pmon_assoc freyd_K_monoidal _ _ _)
41 ; freyd_F_strict_cl : forall a, freyd_F \ #(pmon_cancell freyd_C_monoidal a) ~~ #(pmon_cancell freyd_K_monoidal _)
42 ; freyd_F_strict_cr : forall a, freyd_F \ #(pmon_cancelr freyd_C_monoidal a) ~~ #(pmon_cancelr freyd_K_monoidal _)
44 Coercion freyd_K_monoidal : FreydCategory >-> PreMonoidalCat.
45 Coercion freyd_F : FreydCategory >-> PreMonoidalFunctor.
46 Coercion freyd_K_ : FreydCategory >-> Category.