From 24e35a9f2c84eb167eb2e28c0f5aeb58ee648a58 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 20 Nov 2014 13:37:02 -0500 Subject: [PATCH] fix(hott/trunc): comment out sorry --- library/hott/trunc.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/hott/trunc.lean b/library/hott/trunc.lean index 32babec81..f9df0ac8a 100644 --- a/library/hott/trunc.lean +++ b/library/hott/trunc.lean @@ -178,7 +178,7 @@ namespace truncation definition contr_basedpaths [instance] {A : Type} (a : A) : is_contr (Σ(x : A), a ≈ x) := is_contr.mk (dpair a idp) (λp, sigma.rec_on p (λ b q, path.rec_on q idp)) - definition is_trunc_is_hprop [instance] {n : trunc_index} : is_hprop (is_trunc n A) := sorry + -- definition is_trunc_is_hprop [instance] {n : trunc_index} : is_hprop (is_trunc n A) := sorry definition unit_contr [instance] : is_contr unit := is_contr.mk star (λp, unit.rec_on p idp)