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 RepresentableStructure_ch7_2.
  24
  25 Class GeneralizedArrow (K:Enrichment) {ce}(C:MonoidalEnrichment ce) :=
  26 { ga_functor_obj      : enr_v_mon K -> C
  27 ; ga_functor          : Functor (enr_v_mon K) C ga_functor_obj
  28 ; ga_functor_monoidal : MonoidalFunctor (enr_v_mon K) C ga_functor
  29 }.
  30 Coercion ga_functor_monoidal : GeneralizedArrow >-> MonoidalFunctor.
  31
  32 Implicit Arguments GeneralizedArrow    [ [ce] ].
  33 Implicit Arguments ga_functor_obj      [ K ce C ].
  34 Implicit Arguments ga_functor          [ K ce C ].
  35 Implicit Arguments ga_functor_monoidal [ K ce C ].