Remove contr from equiv

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