From: Auke Booij <auke@tulcod.com>
Date: Thu, 2 Jun 2016 22:44:11 +0000 (+0100)
Subject: Rename truncP to inh
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=ff8a026126d21b917a8bd69c1410ccbddadd0c19;p=cubicaltt.git

Rename truncP to inh
---

diff --git a/examples/propTrunc.ctt b/examples/propTrunc.ctt
index 8ea8f7f..6ba72eb 100644
--- a/examples/propTrunc.ctt
+++ b/examples/propTrunc.ctt
@@ -4,23 +4,23 @@ import prelude
 
 data pTrunc (A : U)
   = inc (a : A)
-  | truncP (x y : pTrunc A) <i> [(i=0) -> x, (i=1) -> y]
+  | inh (x y : pTrunc A) <i> [(i=0) -> x, (i=1) -> y]
 
 pTruncIsProp (A : U) : prop (pTrunc A) =
- \ (x y : pTrunc A) -> <i> truncP{pTrunc A} x y @ i
+ \ (x y : pTrunc A) -> <i> inh{pTrunc A} x y @ i
 
 pTruncRec (A B : U) (pP : prop B) (f : A -> B) : pTrunc A -> B = split
   inc a -> f a
-  truncP x y @ i -> pP (pTruncRec A B pP f x) (pTruncRec A B pP f y) @ i
+  inh x y @ i -> pP (pTruncRec A B pP f x) (pTruncRec A B pP f y) @ i
 
 pTruncElim (A : U) (B : (pTrunc A) -> U)
            (pP : (x : pTrunc A) -> prop (B x))
            (f : (a : A) -> B (inc a))
            : (x : pTrunc A) -> B x = split
   inc a -> f a
-  truncP x y @ i ->
+  inh x y @ i ->
     lemPropF (pTrunc A) B pP x y
-      (<j> truncP{pTrunc A} x y @ j)
+      (<j> inh{pTrunc A} x y @ j)
       (pTruncElim A B pP f x)
       (pTruncElim A B pP f y)
     @ i