From: Anders Mörtberg <mortberg@chalmers.se>
Date: Mon, 13 Apr 2015 21:06:14 +0000 (+0200)
Subject: Remove contr from equiv
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=4254c00daf65366e73f22218064af82a32d7af70;p=cubicaltt.git

Remove contr from equiv
---

diff --git a/examples/equiv.ctt b/examples/equiv.ctt
index d1d860a..321efab 100644
--- a/examples/equiv.ctt
+++ b/examples/equiv.ctt
@@ -2,8 +2,6 @@ module equiv where
 
 import prelude
 
-contr (A:U) : U = (_:A) * prop A
-
 isContr (A : U) : U = and (prop A) A
 
 fiber (A B:U) (f:A->B) (b:B) : U = (x:A) * Id B b (f x)