1 (*********************************************************************************************************************************)
4 (* A reification is a functor R from one enrichING category A to another enrichING category B which forms a commuting square *)
5 (* with every pair of hom-functors Hom(X,-):a->A and Hom(Y,-):b->B up to natural isomorphism. *)
7 (*********************************************************************************************************************************)
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 MonoidalCategories_ch7_8.
22 Require Import Coherence_ch7_8.
23 Require Import Enrichment_ch2_8.
24 Require Import RepresentableStructure_ch7_2.
26 Opaque RepresentableFunctor.
28 Structure Reification (K:Enrichment) (C:Enrichment) (CI:C) :=
29 { reification_r_obj : K -> K -> C
30 ; reification_rstar_obj : enr_v K -> enr_v C
31 ; reification_r : forall k:K, Functor K C (reification_r_obj k)
32 ; reification_rstar_f : Functor (enr_v K) (enr_v C) reification_rstar_obj
33 ; reification_rstar : MonoidalFunctor (enr_v_mon K) (enr_v_mon C) reification_rstar_f
34 ; reification_commutes : ∀ k, reification_r k >>>> RepresentableFunctor C CI <~~~> RepresentableFunctor K k >>>> reification_rstar_f
36 Transparent RepresentableFunctor.
37 Transparent functor_comp.
39 Coercion reification_rstar : Reification >-> MonoidalFunctor.
40 Implicit Arguments Reification [ ].
41 Implicit Arguments reification_r_obj [ K C CI ].
42 Implicit Arguments reification_r [ K C CI ].
43 Implicit Arguments reification_rstar [ K C CI ].
44 Implicit Arguments reification_rstar_f [ K C CI ].
45 Implicit Arguments reification_commutes [ K C CI ].
46 Implicit Arguments reification_rstar_obj [ K C CI ].