From 09b533a965a1968ec8e4cb5cd2e25d774003d0cd Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Wed, 5 Nov 2014 00:10:32 -0500
Subject: [PATCH] fix(library/hott) rename IsEquiv.ap to IsEquiv.ap_closed to
 avoid name clashes

---
 library/hott/equiv.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/hott/equiv.lean b/library/hott/equiv.lean
index 24669790c0..d07a57949d 100644
--- a/library/hott/equiv.lean
+++ b/library/hott/equiv.lean
@@ -210,7 +210,7 @@ namespace IsEquiv
   definition contr (Hf : IsEquiv f) (HA: Contr A) : (Contr B) :=
     Contr.Contr_mk (f (center HA)) (λb, moveR_M Hf (contr HA (inv f b)))
 
-  definition ap (Hf : IsEquiv f) (x y : A) : IsEquiv (@ap A B f x y) := 
+  definition ap_closed (Hf : IsEquiv f) (x y : A) : IsEquiv (@ap A B f x y) := 
     adjointify (ap f) 
       (λq, (inverse (sect f x)) ⬝ ap (f⁻¹) q ⬝ sect f y)
       (λq, !ap_pp