diff --git a/src/HoTTEST/Agda/Exercises/02-Exercises.lagda.md b/src/HoTTEST/Agda/Exercises/02-Exercises.lagda.md index 1303126..6a8ffc3 100644 --- a/src/HoTTEST/Agda/Exercises/02-Exercises.lagda.md +++ b/src/HoTTEST/Agda/Exercises/02-Exercises.lagda.md @@ -178,5 +178,5 @@ Prove that ```agda decidable-equality-char : (A : Type) → has-decidable-equality A ⇔ has-bool-dec-fct A -decidable-equality-char = ? +decidable-equality-char = {! !} ```