X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FReification.v;fp=src%2FReification.v;h=a56ded8e745fd5636585deb80d3302fca990c83d;hp=0000000000000000000000000000000000000000;hb=76f4613eaa5989e29bfd59d716c216ee5386c5f7;hpb=8dc348a407d7a476388401765b24f7815cc801cf

diff --git a/src/Reification.v b/src/Reification.v
new file mode 100644
index 0000000..a56ded8
--- /dev/null
+++ b/src/Reification.v
@@ -0,0 +1,46 @@
+(*********************************************************************************************************************************)
+(* Reification:                                                                                                                  *)
+(*                                                                                                                               *)
+(*   A reification is a functor R from one enrichING category A to another enrichING category B which forms a commuting square   *)
+(*   with every pair of hom-functors Hom(X,-):a->A and Hom(Y,-):b->B up to natural isomorphism.                                  *)
+(*                                                                                                                               *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+Require Import ProductCategories_ch1_6_1.
+Require Import OppositeCategories_ch1_6_2.
+Require Import Enrichment_ch2_8.
+Require Import Subcategories_ch7_1.
+Require Import NaturalTransformations_ch7_4.
+Require Import NaturalIsomorphisms_ch7_5.
+Require Import MonoidalCategories_ch7_8.
+Require Import Coherence_ch7_8.
+Require Import Enrichment_ch2_8.
+Require Import RepresentableStructure_ch7_2.
+
+Opaque RepresentableFunctor.
+Opaque functor_comp.
+Structure Reification (K:Enrichment) (C:Enrichment) (CI:C) :=
+{ reification_r_obj     : K -> K -> C
+; reification_rstar_obj : enr_v K -> enr_v C
+; reification_r         : forall k:K, Functor K C (reification_r_obj k)
+; reification_rstar_f   :             Functor (enr_v K) (enr_v C) reification_rstar_obj
+; reification_rstar     :             MonoidalFunctor (enr_v_mon K) (enr_v_mon C) reification_rstar_f
+; reification_commutes  : forall k, reification_r k >>>> RepresentableFunctor C CI <~~~> RepresentableFunctor K k >>>> reification_rstar_f
+}.
+Transparent RepresentableFunctor.
+Transparent functor_comp.
+
+Coercion reification_rstar : Reification >-> MonoidalFunctor.
+Implicit Arguments Reification                [ ].
+Implicit Arguments reification_r_obj          [ K C CI ].
+Implicit Arguments reification_r              [ K C CI ].
+Implicit Arguments reification_rstar          [ K C CI ].
+Implicit Arguments reification_rstar_f        [ K C CI ].
+Implicit Arguments reification_commutes       [ K C CI ].
+Implicit Arguments reification_rstar_obj      [ K C CI ].