src/GeneralizedArrow.v

   1 (*********************************************************************************************************************************)
   2 (* Generalized Arrow:                                                                                                            *)
   3 (*                                                                                                                               *)
   4 (*   A generalized arrow is a monoidal functor from an enriching category to an enriched category.                               *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   8 Generalizable All Variables.
   9 Require Import Preamble.
  10 Require Import General.
  11 Require Import Categories_ch1_3.
  12 Require Import Functors_ch1_4.
  13 Require Import Isomorphisms_ch1_5.
  14 Require Import ProductCategories_ch1_6_1.
  15 Require Import OppositeCategories_ch1_6_2.
  16 Require Import Enrichment_ch2_8.
  17 Require Import Subcategories_ch7_1.
  18 Require Import NaturalTransformations_ch7_4.
  19 Require Import NaturalIsomorphisms_ch7_5.
  20 Require Import MonoidalCategories_ch7_8.
  21 Require Import Coherence_ch7_8.
  22 Require Import Enrichment_ch2_8.
  23 Require Import Enrichments.
  24 Require Import RepresentableStructure_ch7_2.
  25 Require Import PreMonoidalCenter.
  26 Require Import PreMonoidalCategories.
  27 Require Import BinoidalCategories.
  28
  29 Class GeneralizedArrow (K:Enrichment) {ce}(C:MonoidalEnrichment ce) :=
  30 { ga_functor_obj      : enr_v K -> ce
  31 ; ga_functor          : Functor            (enr_v_mon K) (enr_c_pm ce) ga_functor_obj
  32 ; ga_functor_monoidal : PreMonoidalFunctor (enr_v_mon K) (enr_c_pm ce) ga_functor
  33 (*
  34 ; ga_functor          : Functor         (enr_v_mon K) (Center_is_Monoidal (enr_c_pm ce)) ga_functor_obj
  35 ; ga_functor_monoidal : MonoidalFunctor (enr_v_mon K) (Center_is_Monoidal (enr_c_pm ce)) ga_functor
  36 *)
  37 }.
  38 Coercion ga_functor_monoidal : GeneralizedArrow >-> PreMonoidalFunctor.
  39
  40 Implicit Arguments GeneralizedArrow    [ [ce] ].
  41 Implicit Arguments ga_functor_obj      [ K ce C ].
  42 Implicit Arguments ga_functor          [ K ce C ].
  43 Implicit Arguments ga_functor_monoidal [ K ce C ].