checkpoint

[coq-hetmet.git] / src / WeakFunctorCategory.v

diff --git a/src/WeakFunctorCategory.v b/src/WeakFunctorCategory.v
index 49a5189..85ade61 100644 (file)
--- a/src/WeakFunctorCategory.v
+++ b/src/WeakFunctorCategory.v
@@ -192,8 +192,8 @@ Section WeakFunctorCategoryIsomorphism.
         apply q.
         Defined.
 
         apply q.
         Defined.
 

-    Theorem WeakFunctorCategoriesIsomorphic : IsomorphicCategories GA RE F1 F2.
-      apply Build_IsomorphicCategories.
+    Theorem WeakFunctorCategoriesIsomorphic : IsomorphicCategories GA RE.
+      refine {| ic_f := F1 ; ic_g := F2 |}.

       unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
         eapply if_comp.
         apply m1_m2_id.
       unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *.
         eapply if_comp.
         apply m1_m2_id.