From 4254c00daf65366e73f22218064af82a32d7af70 Mon Sep 17 00:00:00 2001
From: =?utf8?q?Anders=20M=C3=B6rtberg?= <mortberg@chalmers.se>
Date: Mon, 13 Apr 2015 23:06:14 +0200
Subject: [PATCH] Remove contr from equiv

---
 examples/equiv.ctt | 2 --
 1 file changed, 2 deletions(-)

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)
-- 
2.34.1