feat(library/hott): add 'path' namespace

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

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

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
+abbreviation idp {A : Type} {a : A} := idpath a
-notation `idp`:max := idpath _    -- TODO: can we / should we use `1`?
 
-namespace path
+abbreviation induction_on [protected] {A : Type} {a b : A} (p : a ≈ b)
-  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 :=
-    {C : Π (b : A) (p : a ≈ b), Type} (H : C a (idpath a)) : C b p :=
+path.rec H p
-  path.rec H p
-end path
-
-
--- TODO: should all this be in namespace path?
-open path (induction_on)
 
 -- Concatenation and inverse
 -- -------------------------
@@ -693,3 +687,4 @@ Ltac hott_simpl :=
   autorewrite with paths in * |- * ; auto with path_hints.
 
 -/
+end path

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