From ce8ca647719d3820470157f4594a3efd8d5f3c62 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Mon, 25 Jan 2016 16:54:48 +0000
Subject: [PATCH] feat(hott): adjust small things in wedge theory

---
 hott/homotopy/wedge.hlean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/hott/homotopy/wedge.hlean b/hott/homotopy/wedge.hlean
index 2eb6b95d46..103d9596f5 100644
--- a/hott/homotopy/wedge.hlean
+++ b/hott/homotopy/wedge.hlean
@@ -7,11 +7,12 @@ The Wedge Sum of Two Pointed Types
 -/
 import hit.pointed_pushout .connectedness
 
-open eq pushout pointed Pointed
+open eq pushout pointed Pointed unit
 
 definition Wedge (A B : Type*) : Type* := Pushout (pconst Unit A) (pconst Unit B)
 
 namespace wedge
+
   -- TODO maybe find a cleaner proof
   protected definition unit (A : Type*) : A ≃* Wedge Unit A :=
   begin