src/Reification.v

   1 (*********************************************************************************************************************************)
   2 (* Reification:                                                                                                                  *)
   3 (*                                                                                                                               *)
   4 (*   A reification is a functor R from one enrichING category A to another enrichING category B which, for every X, forms        *)
   5 (*   a commuting square with Hom(X,-):a->A and Hom(I,-):b->B (up to natural isomorphism).                                        *)
   6 (*                                                                                                                               *)
   7 (*********************************************************************************************************************************)
   8
   9 Generalizable All Variables.
  10 Require Import Preamble.
  11 Require Import General.
  12 Require Import Categories_ch1_3.
  13 Require Import Functors_ch1_4.
  14 Require Import Isomorphisms_ch1_5.
  15 Require Import ProductCategories_ch1_6_1.
  16 Require Import OppositeCategories_ch1_6_2.
  17 Require Import Enrichment_ch2_8.
  18 Require Import Subcategories_ch7_1.
  19 Require Import NaturalTransformations_ch7_4.
  20 Require Import NaturalIsomorphisms_ch7_5.
  21 Require Import BinoidalCategories.
  22 Require Import PreMonoidalCategories.
  23 Require Import MonoidalCategories_ch7_8.
  24 Require Import Coherence_ch7_8.
  25 Require Import Enrichments.
  26 Require Import Enrichment_ch2_8.
  27 Require Import RepresentableStructure_ch7_2.
  28
  29 Opaque HomFunctor.
  30 Opaque functor_comp.
  31 Structure Reification (K:Enrichment) (C:Enrichment) (CI:C) :=
  32 { reification_r_obj     : K -> K -> C
  33 ; reification_rstar_obj : enr_v K -> enr_v C
  34 ; reification_r         : forall k:K, Functor K C (reification_r_obj k)
  35 ; reification_rstar_f   :             Functor (enr_v K) (enr_v C) reification_rstar_obj
  36 ; reification_rstar     :             PreMonoidalFunctor (enr_v_mon K) (enr_v_mon C) reification_rstar_f
  37 ; reification_commutes  : ∀ k, reification_r k >>>> HomFunctor C CI <~~~> HomFunctor K k >>>> reification_rstar_f
  38
  39 (* We require that the host language (but NOT the guest language) be pure, i.e. all morphisms central, to simplify
  40  * things.  If this doesn't suit you, just consider the "host language" here to be the pure sublanguage of the
  41  * host language, and toss on the inclusion functor to the full language *)
  42 ; reification_host_lang_pure   : CommutativeCat (enr_c_pm C)
  43 }.
  44 Transparent HomFunctor.
  45 Transparent functor_comp.
  46
  47 Coercion reification_rstar : Reification >-> PreMonoidalFunctor.
  48 Implicit Arguments Reification                [ ].
  49 Implicit Arguments reification_r_obj          [ K C CI ].
  50 Implicit Arguments reification_r              [ K C CI ].
  51 Implicit Arguments reification_rstar          [ K C CI ].
  52 Implicit Arguments reification_rstar_f        [ K C CI ].
  53 Implicit Arguments reification_commutes       [ K C CI ].
  54 Implicit Arguments reification_rstar_obj      [ K C CI ].