From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Wed, 2 Dec 2015 20:00:54 +0000 (-0500)
Subject: fix comment
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=70991506721053679bac98a7294759a8f0753b21;p=cubicaltt.git

fix comment
---

diff --git a/examples/setquot.ctt b/examples/setquot.ctt
index 78e6e74..49a3612 100644
--- a/examples/setquot.ctt
+++ b/examples/setquot.ctt
@@ -152,14 +152,13 @@ weqtopathshProp (P P' : hProp) (w : weq P.1 P'.1) : Id hProp P P' =
 
 
 
--- A shorter proof that hProp form a set using univalence:
+-- A short proof that hProp form a set using univalence:
 
 isapropweq (X Y : U) (H : isaprop Y) (f g : weq X Y) : Id (weq X Y) f g =
   equivLemma X Y f g (<i> \(x : X) -> H (f.1 x) (g.1 x) @ i)
 
 isapropidU (X Y : U) : Id U X Y -> isaprop Y -> isaprop X = substInv U isaprop X Y
 
--- isasethProp : isaset hProp
 isasethProp (P P' : hProp) : isaprop (Id hProp P P') =
   isapropidU (Id hProp P P') (weq P.1 P'.1) rem (isapropweq P.1 P'.1 P'.2)
   where