From eee0c59516ebdc929c6d229631cb039408036840 Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Mon, 5 Feb 2024 11:07:02 -0500 Subject: [PATCH] ReflectiveSubuniverse: simplify universe vars in conn_map_homotopic --- theories/Modalities/ReflectiveSubuniverse.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Modalities/ReflectiveSubuniverse.v b/theories/Modalities/ReflectiveSubuniverse.v index 501449ece62..e3dc2124e9a 100644 --- a/theories/Modalities/ReflectiveSubuniverse.v +++ b/theories/Modalities/ReflectiveSubuniverse.v @@ -1605,7 +1605,7 @@ Section ConnectedMaps. Proof. intros ? b. exact (isconnected_equiv O (hfiber@{i i} f b) - (equiv_hfiber_homotopic f g h b) _). + (equiv_hfiber_homotopic@{i i i} f g h b) _). Defined. (** The pullback of a connected map is connected *)