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)(C:Enrichment) :=
  30 { ga_functor_obj      : enr_v K -> C
  31 ; ga_functor          : Functor            (enr_v_mon K) (enr_c_pm C) ga_functor_obj
  32 ; ga_functor_monoidal : PreMonoidalFunctor (enr_v_mon K) (enr_c_pm C) ga_functor
  33
  34 (* We require that the host language (but NOT the guest language) be pure, i.e. all morphisms central, to simplify
  35  * things.  If this doesn't suit you, just consider the "host language" here to be the pure sublanguage of the
  36  * host language, and toss on the inclusion functor to the full language *)
  37 ; ga_host_lang_pure   : CommutativeCat (enr_c_pm C)
  38 }.
  39 Coercion ga_functor_monoidal : GeneralizedArrow >-> PreMonoidalFunctor.
  40
  41 Implicit Arguments GeneralizedArrow    [ ].
  42 Implicit Arguments ga_functor_obj      [ K C ].
  43 Implicit Arguments ga_functor          [ K C ].
  44 Implicit Arguments ga_functor_monoidal [ K C ].