1 (*********************************************************************************************************************************)
2 (* ReificationFromGeneralizedArrow: *)
4 (* Turn a reification into a generalized arrow *)
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 RepresentableStructure_ch7_2.
24 Require Import Reification.
25 Require Import GeneralizedArrow.
27 Definition reification_from_garrow (K:Enrichment) {ce} (C:MonoidalEnrichment ce) (garrow : GeneralizedArrow K C)
28 : Reification K C (mon_i C).
30 {| reification_r := fun k:K => RepresentableFunctor K k >>>> garrow
31 ; reification_rstar_f := garrow >>>> me_mf C
33 apply MonoidalFunctorsCompose.
34 abstract (intros; set (@ni_associativity) as q; apply q).