From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Wed, 6 Jul 2016 11:17:13 +0000 (+0200)
Subject: cleaning in prelude
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=a9993dd3b00a887568f045482b63be2164a9a666;p=cubicaltt.git

cleaning in prelude
---

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index 23bdb3d..4ead1a8 100644
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -136,27 +136,27 @@ prop (A : U) : U = (a b : A) -> Id A a b
 set (A : U) : U = (a b : A) -> prop (Id A a b)
 groupoid (A : U) : U = (a b : A) -> set (Id A a b)
 
-propSet (A : U) (h : prop A) (a b : A) (p q : Id A a b) : Id (Id A a b) p q =
- <j i> comp (<k>A) a [ (i=0) -> h a a
-                , (i=1) -> h a b
-                , (j=0) -> h a (p @ i)
-                , (j=1) -> h a (q @ i)]
-
+propSet (A : U) (h : prop A) : set A =
+ \(a b : A) (p q : Id A a b) ->
+   <j i> comp (<k>A) a [ (i=0) -> h a a
+                       , (i=1) -> h a b
+                       , (j=0) -> h a (p @ i)
+                       , (j=1) -> h a (q @ i)]
 
 propIsProp (A : U) : prop (prop A) =
-  \(f g : prop A) ->
-    <i> \(a b : A) -> (propSet A f a b (f a b) (g a b)) @ i
-
--- propIsProp (A : U) (f g : prop A) : Id (prop A) f g =
---  <i> \(a b :A) -> (propSet A f a b (f a b) (g a b)) @ i
+  \(f g : prop A) -> <i> \(a b : A) ->
+    propSet A f a b (f a b) (g a b) @ i
 
-setIsProp (A : U) (f g : set A) : Id (set A) f g =
- <i> \(a b :A) -> (propIsProp (Id A a b) (f a b) (g a b)) @ i
+setIsProp (A : U) : prop (set A) =
+ \(f g : set A) -> <i> \(a b :A) ->
+   propIsProp (Id A a b) (f a b) (g a b) @ i
 
-IdS (A : U) (P : A -> U) (a0 a1 : A) (p : Id A a0 a1) (u0 : P a0) (u1 : P a1) : U =
-  IdP (<i> P (p @ i)) u0 u1
+IdS (A : U) (P : A -> U) (a0 a1 : A)
+  (p : Id A a0 a1) (u0 : P a0) (u1 : P a1) : U =
+    IdP (<i> P (p @ i)) u0 u1
 
-lemProp (A : U) (h : A -> prop A) : prop A = \ (a : A) -> h a a
+lemProp (A : U) (h : A -> prop A) : prop A =
+  \(a : A) -> h a a
 
 propPi (A : U) (B : A -> U) (h : (x : A) -> prop (B x))
        (f0 f1 : (x : A) -> B x) : Id ((x : A) -> B x) f0 f1