X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FReificationsEquivalentToGeneralizedArrows.v;h=0428638e69ad226b2789d72e1347a387e385700a;hp=1b626a2aea54fdaf4d925436909122d403cd5bc8;hb=e6bd3d7623740382a9af0f6d39e8304b1358d847;hpb=992203bb4a221ea2f415c0d14bb34d35af2ee637

diff --git a/src/ReificationsEquivalentToGeneralizedArrows.v b/src/ReificationsEquivalentToGeneralizedArrows.v
index 1b626a2..0428638 100644
--- a/src/ReificationsEquivalentToGeneralizedArrows.v
+++ b/src/ReificationsEquivalentToGeneralizedArrows.v
@@ -52,23 +52,22 @@ Section ReificationsEquivalentToGeneralizedArrows.
     Qed.
 
   Definition roundtrip_lemma
-    (K:SurjectiveEnrichment) (C:MonicMonoidalEnrichment) (reification : Reification K C (me_i C))
+    `(K:SurjectiveEnrichment se) `(C:MonicMonoidalEnrichment e ce) (reification : Reification K C (me_i C))
     := roundtrip_lemma' (RepresentableFunctor C (me_i C)) (ffme_mf_full C) (ffme_mf_faithful C) (step1_functor K C reification).
 
   Lemma roundtrip_reification_to_reification
-    (K:SurjectiveEnrichment) (C:MonicMonoidalEnrichment) (reification : Reification K C (me_i C))
+    `(K:SurjectiveEnrichment se) `(C:MonicMonoidalEnrichment e ce) (reification : Reification K C (me_i C))
     : reification ≃ reification_from_garrow K C (garrow_from_reification K C reification).
     simpl.
     unfold mon_f.
     unfold garrow_functor.
     apply (if_comp(F2:=(step1_functor K C reification >>>> InclusionFunctor _ (FullImage (RepresentableFunctor C (me_i C)))))).
-       apply step1_niso.
+       apply (@step1_niso _ K _ _ C reification).
        apply (if_inv (roundtrip_lemma K C reification)).
     Qed.
-    (* FIXME: show that the R-functors are naturally isomorphic as well; should follow pretty easily from the proof for Rstar *)
 
   Lemma roundtrip_garrow_to_garrow
-    (K:SurjectiveEnrichment) (C:MonicMonoidalEnrichment) (garrow : GeneralizedArrow K C)
+    `(K:SurjectiveEnrichment se) `(C:MonicMonoidalEnrichment e ce) (garrow : GeneralizedArrow K C)
     : garrow ≃ garrow_from_reification K C (reification_from_garrow K C garrow).
     apply (ffc_functor_weakly_monic _ (ffme_mf_conservative C)).
     apply if_inv.
@@ -78,13 +77,10 @@ Section ReificationsEquivalentToGeneralizedArrows.
     unfold garrow_from_reification.
     unfold garrow_functor.
     unfold step2_functor.
-    apply roundtrip_lemma.
+    set (@roundtrip_lemma _ K _ _ C) as q.
+    apply (q (reification_from_garrow K C garrow)).
     apply if_inv.
     apply (step1_niso K C (reification_from_garrow K C garrow)).
     Qed.
 
-  Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfReifications CategoryOfGeneralizedArrows.
-    admit.
-    Qed.
-
 End ReificationsEquivalentToGeneralizedArrows.