From 70991506721053679bac98a7294759a8f0753b21 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Wed, 2 Dec 2015 15:00:54 -0500 Subject: [PATCH] fix comment --- examples/setquot.ctt | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) 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 ( \(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 -- 2.34.1