From 8e1949e9aa6170f961d68d863db205547e87a1f8 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Thu, 6 Nov 2014 11:20:01 -0500
Subject: [PATCH] feat(library/hott) add calc environment for equivalences

---
 library/hott/equiv.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/library/hott/equiv.lean b/library/hott/equiv.lean
index 4877147af..c520f7a28 100644
--- a/library/hott/equiv.lean
+++ b/library/hott/equiv.lean
@@ -282,6 +282,13 @@ namespace Equiv
   theorem contr_closed (HA: Contr A) : (Contr B) :=
     @IsEquiv.contr A B (equiv_fun eqf) (equiv_isequiv eqf) HA
 
+  -- calc enviroment
+  -- TODO: find a transport lemma?
+  -- calc_subst transport
+  calc_trans compose
+  calc_refl id
+  calc_symm inv_closed
+
 end Equiv
 
 namespace Equiv