X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FRepresentableStructure_ch7_2.v;fp=src%2FRepresentableStructure_ch7_2.v;h=dfd04b5f1545e1ed3111b32b09725466b9c20ed4;hp=da3f519e76c7f9a629535569f63d9aed9ddc0b64;hb=95fb933d1021113abadc4a71cc19d19ea2fd4781;hpb=00b060e4854e5a1ba01746be44ac9deb49d7fbf5

diff --git a/src/RepresentableStructure_ch7_2.v b/src/RepresentableStructure_ch7_2.v
index da3f519..dfd04b5 100644
--- 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.