src/ReificationFromGeneralizedArrow.v

   1 (*********************************************************************************************************************************)
   2 (* ReificationFromGeneralizedArrow:                                                                                              *)
   3 (*                                                                                                                               *)
   4 (*   Turn a reification into a generalized arrow                                                                                 *)
   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 Require Import Reification.
  25 Require Import GeneralizedArrow.
  26
  27 Definition reification_from_garrow (K:Enrichment) {ce} (C:MonoidalEnrichment ce) (garrow : GeneralizedArrow K C)
  28  : Reification K C (mon_i C).
  29   refine
  30   {| reification_r         := fun k:K => HomFunctor K k >>>> garrow
  31    ; reification_rstar_f   :=                                garrow >>>> me_mf C
  32    ; reification_rstar     := MonoidalFunctorsCompose _ _ _ _ _ garrow (me_mf C)
  33    |}.
  34    abstract (intros; set (@ni_associativity) as q; apply q).
  35    Defined.
  36
  37
  38