comment out unused portion of RepresentableStructure_ch7_2

[coq-categories.git] / src / RepresentableStructure_ch7_2.v

diff --git a/src/RepresentableStructure_ch7_2.v b/src/RepresentableStructure_ch7_2.v
index da3f519..dfd04b5 100644 (file)
--- a/src/RepresentableStructure_ch7_2.v
+++ b/src/RepresentableStructure_ch7_2.v
@@ -106,6 +106,7 @@ Section RepresentableStructure.
       apply hom_covariant_distributes.
       Defined.
 
+  (*
   Lemma undo_homfunctor `(f:a~~{ec}~~>b) : f ~~ eid _ >>> (HomFunctor a \ f).
     simpl.
     setoid_rewrite <- associativity.
@@ -143,7 +144,7 @@ Section RepresentableStructure.
     set (@eqv_equivalence) as qmt.
     apply qmt.
     Qed.
-
+    *)
 
 End RepresentableStructure.
 Opaque HomFunctor.