From: Apostolis Xekoukoulotakis <apostolis.xekoukoulotakis@gmail.com>
Date: Sun, 17 Sep 2017 07:05:30 +0000 (+0300)
Subject: A small simplification on binnat.ctt
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=423577ea49790bab2113c8d69ff8f9b6483a6015;p=cubicaltt.git

A small simplification on binnat.ctt
---

diff --git a/examples/binnat.ctt b/examples/binnat.ctt
index f156ef0..3c0ef3f 100644
--- a/examples/binnat.ctt
+++ b/examples/binnat.ctt
@@ -211,10 +211,8 @@ eqDouble2 : Path Double DoubleBinN' DoubleBinN
      rem1 : (n : binN) -> Path binN (doubleBinN' n) (doubleBinN n)
       = split
       binN0     -> <_> binN0
-      binNpos p -> <i> comp (<_> binN) (NtoBinN (doubleN (PosToN p)))
-                          [ (i=0) -> <_> NtoBinN (doubleN (PosToN p))
-                          , (i=1) -> lem1 (x0 p) ]
-
+      binNpos p -> lem1 (x0 p)
+      
 eqDouble : Path Double DoubleN DoubleBinN =
   compPath Double DoubleN DoubleBinN' DoubleBinN eqDouble1 eqDouble2