From: Anders Mörtberg 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 = - comp (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) -> + comp (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) -> - \(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 = --- \(a b :A) -> (propSet A f a b (f a b) (g a b)) @ i + \(f g : prop A) -> \(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 = - \(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) -> \(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 ( 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 ( 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