--- /dev/null
+(*******************************************************************************)
+(* Freyd Categories *)
+(*******************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+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 NaturalIsomorphisms_ch7_5.
+Require Import Coherence_ch7_8.
+Require Import MonoidalCategories_ch7_8.
+
+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_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.