From e095fbaf4b44ea2f9be9c951e23293714d807665 Mon Sep 17 00:00:00 2001
From: Russell McClellan <russell.mcclellan@gmail.com>
Date: Sat, 4 Dec 2021 20:07:03 -0500
Subject: [PATCH] fix missing definition in solutions

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

diff --git a/1FundamentalGroup/Quest0Solutions.agda b/1FundamentalGroup/Quest0Solutions.agda
index 6ac2880..5415de5 100644
--- a/1FundamentalGroup/Quest0Solutions.agda
+++ b/1FundamentalGroup/Quest0Solutions.agda
@@ -43,7 +43,7 @@ pathEmpty : (A : Type) → Type₁
 pathEmpty A = A ≡ ⊥
 
 isoEmpty : (A : Type) → Type
-isoEmpty A = {!!}
+isoEmpty A = A ≅ ⊥
 
 outOf⊥ : (A : Type) → ⊥ → A
 outOf⊥ A ()