From f76c9575a5d9fa0e7d2b4c57c86245c46f8b422a Mon Sep 17 00:00:00 2001
From: =?utf8?q?Anders=20M=C3=B6rtberg?= <andersmortberg@gmail.com>
Date: Thu, 14 Jan 2016 22:44:12 -0500
Subject: [PATCH] one less undefined

---
 examples/setquot.ctt | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/examples/setquot.ctt b/examples/setquot.ctt
index 06656ec..ec2db10 100644
--- a/examples/setquot.ctt
+++ b/examples/setquot.ctt
@@ -213,7 +213,8 @@ weqpathsinsetquot (X : U) (R : eqrel X) (x x' : X) :
              (R.1 x x').1 = transport (<i> (rem1 @ i).1) rem
            where
            rem : (R.1 x' x').1 = eqrelrefl X R x'
-           rem1 : Id hProp (R.1 x' x') (R.1 x x') = undefined
+           rem2 : Id hProp (R.1 x x') (R.1 x' x') = <i> (e @ i).1 x'
+           rem1 : Id hProp (R.1 x' x') (R.1 x x') = <i> rem2 @ -i
          pA : prop (R.1 x x').1 = (R.1 x x').2
          pB : prop (Id (setquot X R.1) (setquotpr X R x) (setquotpr X R x')) = setsetquot X R.1 (setquotpr X R x) (setquotpr X R x')
 
-- 
2.34.1