fix unfolding in proof of isconnected_fiber_to_cofiber

Signed-off-by: Ali Caglayan <alizter@gmail.com>
HoTT · Jan 28, 2025 · 7aa3b08 · 7aa3b08
1 parent dca49f9
commit 7aa3b08
Showing 1 changed file with 3 additions and 3 deletions.
diff --git 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.