From 68587ee51cbd3d97651f18c703af2ac91c399234 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sun, 26 Feb 2023 18:41:31 -0500
Subject: [PATCH] Connectedness.v: remove a universe variable from
 conn_point_incl

---
 theories/Truncations/Connectedness.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/Truncations/Connectedness.v b/theories/Truncations/Connectedness.v
index fbfaf91875a..7e21dbc0039 100644
--- a/theories/Truncations/Connectedness.v
+++ b/theories/Truncations/Connectedness.v
@@ -77,8 +77,9 @@ Definition conn_point_incl `{Univalence} {n : trunc_index} {A : Type@{u}} (a0:A)
            `{IsConnected n.+1 A}
   : IsConnMap n (unit_name a0).
 Proof.
-  (* Coq can find [conn_map_to_unit_isconnected] via typeclass search, but we manually pose it to get rid of an unneeded universe variable. *)
+  (* Coq can find [conn_map_to_unit_isconnected] and [isconnected_contr] via typeclass search, but we manually pose them to get rid of an unneeded universe variable. *)
   pose conn_map_to_unit_isconnected@{u u}.
+  pose isconnected_contr@{u u}.
   rapply (OO_cancelL_conn_map@{u u u u} (Tr n.+1) (Tr n) (unit_name a0) (const_tt A)).
   apply O_lex_leq_Tr.
 Defined.