From 95fb933d1021113abadc4a71cc19d19ea2fd4781 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Tue, 29 Mar 2011 06:34:59 -0700 Subject: [PATCH] comment out unused portion of RepresentableStructure_ch7_2 --- src/RepresentableStructure_ch7_2.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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. -- 1.7.10.4