From 622aa74d91c8f1499f82ed19e020c8aa26ddf2d4 Mon Sep 17 00:00:00 2001
From: Ingo Blechschmidt <iblech@speicherleck.de>
Date: Fri, 19 Jan 2024 15:09:58 +0100
Subject: [PATCH] compatibility with recent cubical

---
 1FundamentalGroup/Preambles/P0.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/1FundamentalGroup/Preambles/P0.agda b/1FundamentalGroup/Preambles/P0.agda
index 13e74e3..9dc6726 100644
--- a/1FundamentalGroup/Preambles/P0.agda
+++ b/1FundamentalGroup/Preambles/P0.agda
@@ -2,7 +2,7 @@ module 1FundamentalGroup.Preambles.P0 where
 
 open import Cubical.Data.Empty using (⊥) public
 open import Cubical.Data.Unit renaming ( Unit to ⊤ ) public
-open import Cubical.Data.Bool public
+open import Cubical.Data.Bool hiding (elim) public
 open import Cubical.Foundations.Prelude
      renaming ( subst to endPt
               ; transport to pathToFun