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 PreMonoidalCategories.
  21 Require Import MonoidalCategories_ch7_8.
  22 Require Import Coherence_ch7_8.
  23 Require Import Enrichment_ch2_8.
  24 Require Import Enrichments.
  25 Require Import RepresentableStructure_ch7_2.
  26 Require Import Reification.
  27 Require Import GeneralizedArrow.
  28
  29 Definition reification_from_garrow (K:Enrichment) {ce} (C:MonoidalEnrichment ce) (garrow : GeneralizedArrow K ce)
  30  : Reification K ce (enr_c_i ce).
  31   refine
  32   {| reification_r         := fun k:K => HomFunctor K k >>>> ga_functor garrow
  33    ; reification_rstar_f   :=                                ga_functor garrow >>>> C
  34    ; reification_rstar     := PreMonoidalFunctorsCompose garrow C
  35    |}.
  36    abstract (intros; set (@ni_associativity) as q; apply q).
  37    intros; apply ga_host_lang_pure.
  38    Defined.
  39
  40
  41