From ff8a026126d21b917a8bd69c1410ccbddadd0c19 Mon Sep 17 00:00:00 2001 From: Auke Booij Date: Thu, 2 Jun 2016 23:44:11 +0100 Subject: [PATCH] Rename truncP to inh --- examples/propTrunc.ctt | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) 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=0) -> x, (i=1) -> y] + | inh (x y : pTrunc A) [(i=0) -> x, (i=1) -> y] pTruncIsProp (A : U) : prop (pTrunc A) = - \ (x y : pTrunc A) -> truncP{pTrunc A} x y @ i + \ (x y : pTrunc A) -> 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 - ( truncP{pTrunc A} x y @ j) + ( inh{pTrunc A} x y @ j) (pTruncElim A B pP f x) (pTruncElim A B pP f y) @ i -- 2.34.1