src/FreydCategories.v

   1 (*******************************************************************************)
   2 (* Freyd Categories                                                            *)
   3 (*******************************************************************************)
   4
   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.
  18
  19 Class FreydCategory
  20 { Ob                          :  Type                                   }
  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                )
  29 :=
  30 { freyd_K_                    := freyd_K
  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 _)
  43 }.
  44 Coercion freyd_K_monoidal : FreydCategory >-> PreMonoidalCat.
  45 Coercion freyd_F          : FreydCategory >-> PreMonoidalFunctor.
  46 Coercion freyd_K_         : FreydCategory >-> Category.