diff --git a/1FundamentalGroup/Quest0Solutions.agda b/1FundamentalGroup/Quest0Solutions.agda index 5415de5..6ac2880 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 = A ≅ ⊥ +isoEmpty A = {!!} outOf⊥ : (A : Type) → ⊥ → A outOf⊥ A ()