X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FRepresentableStructure_ch7_2.v;h=2cfe5ebb75d764e1bd29c3f8cb534a78c829cb18;hp=3dd7b78f6e701c65b3149e190f96503c17faefc4;hb=27ffdd2265eb1c15acc62970f49d25a07bcadb05;hpb=ff3003c261295c60d367580b6700396102eb5a9c

diff --git a/src/RepresentableStructure_ch7_2.v b/src/RepresentableStructure_ch7_2.v
index 3dd7b78..2cfe5eb 100644
--- a/src/RepresentableStructure_ch7_2.v
+++ b/src/RepresentableStructure_ch7_2.v
@@ -7,6 +7,7 @@ Require Import Preamble.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.
+Require Import EpicMonic_ch2_1.
 Require Import ProductCategories_ch1_6_1.
 Require Import OppositeCategories_ch1_6_2.
 Require Import Enrichment_ch2_8.
@@ -15,14 +16,15 @@ Require Import NaturalTransformations_ch7_4.
 Require Import NaturalIsomorphisms_ch7_5.
 Require Import MonoidalCategories_ch7_8.
 Require Import Coherence_ch7_8.
-
-(* FIXME: an object is a Generator if its covariant representable functor is faithful *)
+Require Import BinoidalCategories.
+Require Import PreMonoidalCategories.
+Require Import MonoidalCategories_ch7_8.
 
 Section RepresentableStructure.
   Context `(ec:ECategory(mn:=mn)(V:=V)).
 
-  Definition hom_contravariant {a:ec}{d e:ec}(f:EI~~{V}~~>(d~~>e)) := #(pmon_cancell mn _)⁻¹ >>> (f ⋉ (_ ~~> a)) >>> ecomp.
-  Definition hom_covariant     {a:ec}{d e:ec}(f:EI~~{V}~~>(d~~>e)) := #(pmon_cancelr mn _)⁻¹ >>> ((a ~~> d) ⋊ f) >>> ecomp.
+  Definition hom_contravariant {a:ec}{d e:ec}(f:EI~~{V}~~>(d~~>e)) := #(pmon_cancell _)⁻¹ >>> (f ⋉ (_ ~~> a)) >>> ecomp.
+  Definition hom_covariant     {a:ec}{d e:ec}(f:EI~~{V}~~>(d~~>e)) := #(pmon_cancelr _)⁻¹ >>> ((a ~~> d) ⋊ f) >>> ecomp.
 
   Lemma hom_covariant_distributes     {a b c:ec}{x}(f:a~~{ec}~~>b)(g:b~~{ec}~~>c)
      : hom_covariant (f >>> g) ~~ (hom_covariant (a:=x) f) >>> (hom_covariant g).
@@ -35,24 +37,13 @@ Section RepresentableStructure.
      apply qq.
      Qed.
 
-  Lemma hom_contravariant_distributes {a b c:ec}{x}(f:a~~{ec}~~>b)(g:b~~{ec}~~>c)
-     : hom_contravariant (f >>> g) ~~ (hom_contravariant g) >>> (hom_contravariant (a:=x) f).
-     set (f >>> g) as fg; simpl in fg; unfold fg; clear fg.
-     unfold hom_contravariant.
-     repeat setoid_rewrite associativity.
-     etransitivity; [ idtac | symmetry; apply associativity ].
-     apply comp_respects; try reflexivity.
-     set (@ecomp_is_functorial _ _ _ _ _ _ _ _ _ _ _ _ _ x f g) as qq.
-     setoid_rewrite juggle2 in qq.
-     admit.
-     Qed.
-
+  (*
   Lemma hom_swap {a b c d:ec}(f:a~~{ec}~~>b)(g:c~~{ec}~~>d)
      : hom_covariant f >>> hom_contravariant g ~~ hom_contravariant g >>> hom_covariant f.
      etransitivity.
      unfold hom_covariant.
      unfold hom_contravariant.
-     Admitted.
+     Defined.     
 
   Definition YonedaBiFunctor_fmor (a b:ec⁽ºᑭ⁾ ×× ec)(f:a~~{ec⁽ºᑭ⁾ ×× ec}~~>b)
         : ((fst_obj _ _ a)~~>(snd_obj _ _ a))~~{V}~~>((fst_obj _ _ b)~~>(snd_obj _ _ b)).
@@ -94,11 +85,32 @@ Section RepresentableStructure.
               reflexivity).
     Defined.
 
-  Definition RepresentableFunctorºᑭ (X:ec) : Functor ec⁽ºᑭ⁾ V (fun a => a~~>X) := func_rlecnac X >>>> YonedaBiFunctor.
-  Definition RepresentableFunctor   (X:ec) : Functor ec     V (fun a => X~~>a) :=
-    func_llecnac(C:=ec⁽ºᑭ⁾)(D:=ec) X >>>> YonedaBiFunctor.
-  
-  Lemma undo_homfunctor `(f:a~~{ec}~~>b) : f ~~ eid _ >>> (RepresentableFunctor a \ f).
+  Definition HomFunctorºᑭ (X:ec) : Functor ec⁽ºᑭ⁾ V (fun a => a~~>X) := func_rlecnac X >>>> YonedaBiFunctor.
+  *)
+
+  Definition HomFunctor   (X:ec) : Functor ec     V (ehom X).
+    refine {| fmor := @hom_covariant X |}.
+    intros.
+      unfold hom_covariant.
+      apply comp_respects; try reflexivity.
+      apply comp_respects; try reflexivity.
+      apply fmor_respects; auto.
+    intros.
+      unfold hom_covariant.
+      apply (epic _ (iso_epic ((pmon_cancelr) (X ~~> a)))).
+      setoid_rewrite <- associativity.
+      setoid_rewrite <- associativity.
+      setoid_rewrite iso_comp1.
+      setoid_rewrite left_identity.
+      setoid_rewrite right_identity.
+      apply (@eright_identity).
+    intros.
+      symmetry.
+      apply hom_covariant_distributes.
+      Defined.
+
+  (*
+  Lemma undo_homfunctor `(f:a~~{ec}~~>b) : f ~~ eid _ >>> (HomFunctor a \ f).
     simpl.
     setoid_rewrite <- associativity.
     unfold hom_contravariant.
@@ -135,28 +147,8 @@ Section RepresentableStructure.
     set (@eqv_equivalence) as qmt.
     apply qmt.
     Qed.
-
+    *)
 
 End RepresentableStructure.
-Opaque RepresentableFunctor.
-
-Structure MonoidalEnrichment :=
-{ me_enr         : Enrichment
-; me_fobj        : prod_obj me_enr me_enr -> me_enr
-; me_f           : Functor (me_enr ×× me_enr) me_enr me_fobj
-; me_i           : me_enr
-; me_mon         : MonoidalCat me_enr me_fobj me_f me_i
-; me_mf          : MonoidalFunctor me_mon (enr_v_mon me_enr) (RepresentableFunctor me_enr me_i)
-}.
-Coercion me_mon : MonoidalEnrichment >-> MonoidalCat.
-Coercion me_enr : MonoidalEnrichment >-> Enrichment.
+Opaque HomFunctor.
 
-(* an enrichment for which hom(I,-) is monoidal, full, faithful, and conservative *)
-Structure MonicMonoidalEnrichment :=
-{ ffme_enr             : MonoidalEnrichment
-; ffme_mf_full         : FullFunctor         (RepresentableFunctor ffme_enr (me_i ffme_enr))
-; ffme_mf_faithful     : FaithfulFunctor     (RepresentableFunctor ffme_enr (me_i ffme_enr))
-; ffme_mf_conservative : ConservativeFunctor (RepresentableFunctor ffme_enr (me_i ffme_enr))
-}.
-Coercion ffme_enr : MonicMonoidalEnrichment >-> MonoidalEnrichment.
-Transparent RepresentableFunctor.