1 (*********************************************************************************************************************************)
2 (* Generalized Arrow: *)
4 (* A generalized arrow is a monoidal functor from an enriching category to an enriched category. *)
6 (*********************************************************************************************************************************)
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.
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
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
38 Coercion ga_functor_monoidal : GeneralizedArrow >-> PreMonoidalFunctor.
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 ].