From 3a09e743a2fda860f8e8290c032f97ff452825a2 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Tue, 23 Jan 2018 12:47:29 -0500 Subject: [PATCH] fix error in EM --- homotopy/EM.hlean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/homotopy/EM.hlean b/homotopy/EM.hlean index d723a54..6b05571 100644 --- a/homotopy/EM.hlean +++ b/homotopy/EM.hlean @@ -530,7 +530,7 @@ namespace EM refine isomorphism_of_eq (ap (λx, πg[x+1] X) !zero_add⁻¹) ⬝g homotopy_group_add X 0 n ⬝g _ ⬝g !fundamental_group_EM1, exact homotopy_group_isomorphism_of_pequiv 0 e, - refine is_trunc_of_is_trunc_loopn n 1 X _ _, + refine is_trunc_of_is_trunc_loopn n 1 X _ (@is_conn_of_is_conn_succ _ _ H1), apply is_trunc_equiv_closed_rev 1 e end