From 38a4852e7d21ee923109d525b310510b076d360b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 9 Sep 2014 13:20:04 -0700
Subject: [PATCH] feat(library/hott): add 'path' namespace

---
 library/hott/equiv.lean  |  2 +-
 library/hott/funext.lean |  2 +-
 library/hott/path.lean   | 17 ++++++-----------
 library/hott/trunc.lean  |  3 +--
 4 files changed, 9 insertions(+), 15 deletions(-)

diff --git a/library/hott/equiv.lean b/library/hott/equiv.lean
index 470e718ba..9d01d64df 100644
--- a/library/hott/equiv.lean
+++ b/library/hott/equiv.lean
@@ -2,8 +2,8 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Jeremy Avigad
 -- Ported from Coq HoTT
-
 import .path
+open path
 
 -- Equivalences
 -- ------------
diff --git a/library/hott/funext.lean b/library/hott/funext.lean
index 272de72bb..f204af9f0 100644
--- a/library/hott/funext.lean
+++ b/library/hott/funext.lean
@@ -5,8 +5,8 @@
 
 -- TODO: move this to an "axioms" folder
 -- TODO: take a look at the Coq tricks
-
 import .path .equiv
+open path
 
 -- Funext
 -- ------
diff --git a/library/hott/path.lean b/library/hott/path.lean
index 9d087fc69..7766c86d5 100644
--- a/library/hott/path.lean
+++ b/library/hott/path.lean
@@ -18,20 +18,14 @@ open function
 inductive path {A : Type} (a : A) : A → Type :=
 idpath : path a a
 
+namespace path
 infix `≈` := path
 notation x `≈` y:50 `:>`:0 A:0 := @path A x y    -- TODO: is this right?
-abbreviation idpath := @path.idpath
-notation `idp`:max := idpath _    -- TODO: can we / should we use `1`?
+abbreviation idp {A : Type} {a : A} := idpath a
 
-namespace path
-  abbreviation induction_on [protected] {A : Type} {a b : A} (p : a ≈ b)
-    {C : Π (b : A) (p : a ≈ b), Type} (H : C a (idpath a)) : C b p :=
-  path.rec H p
-end path
-
-
--- TODO: should all this be in namespace path?
-open path (induction_on)
+abbreviation induction_on [protected] {A : Type} {a b : A} (p : a ≈ b)
+  {C : Π (b : A) (p : a ≈ b), Type} (H : C a (idpath a)) : C b p :=
+path.rec H p
 
 -- Concatenation and inverse
 -- -------------------------
@@ -693,3 +687,4 @@ Ltac hott_simpl :=
   autorewrite with paths in * |- * ; auto with path_hints.
 
 -/
+end path
diff --git a/library/hott/trunc.lean b/library/hott/trunc.lean
index c0ee4f54d..d5c736c34 100644
--- a/library/hott/trunc.lean
+++ b/library/hott/trunc.lean
@@ -2,9 +2,8 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Jeremy Avigad
 -- Ported from Coq HoTT
-
 import .path
-
+open path
 
 -- Truncation levels
 -- -----------------