From 7aa3b085ea1311f0ff12a858ee2cf6d78b730a23 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Tue, 28 Jan 2025 11:43:18 +0100 Subject: [PATCH] fix unfolding in proof of isconnected_fiber_to_cofiber Signed-off-by: Ali Caglayan --- theories/Homotopy/Cofiber.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/Homotopy/Cofiber.v b/theories/Homotopy/Cofiber.v index 264aa47c6c..55334efd1f 100644 --- a/theories/Homotopy/Cofiber.v +++ b/theories/Homotopy/Cofiber.v @@ -151,8 +151,8 @@ Proof. 1: reflexivity. snrapply path_sigma. 1: reflexivity. - simpl. + unfold fiber_to_path_cofiber; simpl. lhs_V nrapply inv_V. - change ((pglue ?x)^^ = ?y) with ((cfglue f x)^ = y). - by elim (cfglue f x). + nrapply ap; symmetry. + apply concat_1p. Defined.