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 ()