From 11d587cf2a584dd1e09318b68bf78cbb2166d29c Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Tue, 25 Jun 2024 16:46:47 -0500
Subject: [PATCH] ex2

---
 src/HoTTEST/Agda/Exercises/02-Exercises.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 = {!   !}
 ```