From d10e5805a2aecb283e61f625e9d0be295dd9ac28 Mon Sep 17 00:00:00 2001
From: jlh <48520973+Jlh18@users.noreply.github.com>
Date: Wed, 30 Mar 2022 15:55:34 +0100
Subject: [PATCH] Update Quest4Solutions.agda

---
 0Trinitarianism/Quest4Solutions.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/0Trinitarianism/Quest4Solutions.agda b/0Trinitarianism/Quest4Solutions.agda
index 6e1e9bc..6eaa5f0 100644
--- a/0Trinitarianism/Quest4Solutions.agda
+++ b/0Trinitarianism/Quest4Solutions.agda
@@ -44,7 +44,7 @@ rfl* p = rfl
 *Sym : (p : Id x y) → Id (p * Sym p) rfl
 *Sym rfl = rfl
 
-Sym* : (p : Id x y) → Id rfl (p * Sym p)
+Sym* : {A : Type} {x y : A} (p : Id x y) → Id (Sym p * p) rfl
 Sym* rfl = rfl
 
 Assoc : (p : Id w x) (q : Id x y) (r : Id y z)