From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Fri, 15 Jan 2016 03:44:12 +0000 (-0500)
Subject: one less undefined
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=f76c9575a5d9fa0e7d2b4c57c86245c46f8b422a;p=cubicaltt.git

one less undefined
---

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')