src/FreydCategories.v

   1 (*******************************************************************************)
   2 (* Freyd Categories                                                            *)
   3 (*******************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Notations.
   7 Require Import Categories_ch1_3.
   8 Require Import Functors_ch1_4.
   9 Require Import Isomorphisms_ch1_5.
  10 Require Import ProductCategories_ch1_6_1.
  11 Require Import InitialTerminal_ch2_2.
  12 Require Import Subcategories_ch7_1.
  13 Require Import NaturalTransformations_ch7_4.
  14 Require Import NaturalIsomorphisms_ch7_5.
  15 Require Import Coherence_ch7_8.
  16 Require Import BinoidalCategories.
  17 Require Import PreMonoidalCategories.
  18 Require Import PreMonoidalCenter.
  19 Require Import MonoidalCategories_ch7_8.
  20
  21 (* A Freyd Category is... *)
  22 Class FreydCategory
  23
  24    (* a cartesian category C *)
  25   `(C:CartesianCat(Ob:=Ob)(C:=C1)(bin_obj':=bobj))
  26
  27    (* a premonoidal category K with the same objects (its unit object is 1 because the functor is both IIO and strict) *)
  28   `(K:PreMonoidalCat(Ob:=Ob)(bin_obj':=bobj)(I:=pmon_I C))
  29
  30    (* an identity-on-objects functor J:C->Z(K) *)
  31 := { fc_J       : Functor C (Center_is_Monoidal K) (fun x => x)
  32
  33    (* which is a monoidal functor *)
  34    ; fc_mf_J    : MonoidalFunctor C (Center_is_Monoidal K) fc_J
  35
  36    (* and strict (meaning the functor's coherence maps are identities) *)
  37    ; fc_strict_first   : forall a b, #(mf_first(PreMonoidalFunctor:=fc_mf_J) a b) ~~ id _  (* mf_consistent gives us mf_second *)
  38    ; fc_strict_id      : #(mf_i(PreMonoidalFunctor:=fc_mf_J)) ~~ id _
  39
  40    ; fc_C       := C
  41    ; fc_K       := K
  42    }.
  43
  44 Coercion fc_mf_J   : FreydCategory >-> MonoidalFunctor.
  45 Coercion fc_K      : FreydCategory >-> PreMonoidalCat.
  46