From: Adam Megacz <adam@megacz.com>
Date: Tue, 29 Mar 2011 13:34:59 +0000 (-0700)
Subject: comment out unused portion of RepresentableStructure_ch7_2
X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=commitdiff_plain;h=95fb933d1021113abadc4a71cc19d19ea2fd4781

comment out unused portion of RepresentableStructure_ch7_2
---

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.