feat(hott.init): define core namespace

hott/init/default.hlean

@@ -13,3 +13,13 @@ import init.types
 import init.trunc init.path init.equiv init.util
 import init.ua init.funext
 import init.hedberg init.nat init.hit
+
+namespace core
+  export bool empty unit sum sigma
+  export [notations] prod
+  export eq (idp idpath concat inverse transport ap ap10 cast tr_inv homotopy ap11 apd)
+  export [declarations] function
+  export equiv (to_inv to_right_inv to_left_inv)
+  export is_equiv (inv right_inv left_inv)
+
+end core

hott/init/equiv.hlean

@@ -62,6 +62,7 @@ namespace is_equiv
                )
 
   -- Any function equal to an equivalence is an equivlance as well.
+  variable {f}
   definition is_equiv_eq_closed [Hf : is_equiv f] (Heq : f = f') : (is_equiv f') :=
      eq.rec_on Heq Hf
 
@@ -146,7 +147,7 @@ namespace is_equiv
   include Hf
 
   --The inverse of an equivalence is, again, an equivalence.
-  definition is_equiv_inv [instance] : (is_equiv f⁻¹) :=
+  definition is_equiv_inv [instance] : is_equiv f⁻¹ :=
   adjointify f⁻¹ f (left_inv f) (right_inv f)
 
   definition cancel_right (g : B → C) [Hgf : is_equiv (g ∘ f)] : (is_equiv g) :=
@@ -249,8 +250,8 @@ namespace equiv
   protected definition trans (f : A ≃ B) (g: B ≃ C) : A ≃ C :=
   equiv.mk (g ∘ f) !is_equiv_compose
 
-  definition equiv_of_eq_fn_of_equiv (f : A ≃ B) (f' : A → B) (Heq : f = f') : A ≃ B :=
-  equiv.mk f' (is_equiv_eq_closed f Heq)
+  definition equiv_of_eq_fn_of_equiv (f : A ≃ B) {f' : A → B} (Heq : f = f') : A ≃ B :=
+  equiv.mk f' (is_equiv_eq_closed Heq)
 
   definition eq_equiv_fn_eq (f : A → B) [H : is_equiv f] (a b : A) : (a = b) ≃ (f a = f b) :=
   equiv.mk (ap f) !is_equiv_ap

hott/init/funext.hlean

@@ -10,7 +10,7 @@ Ported from Coq HoTT
 
 prelude
 import .trunc .equiv .ua
-open eq is_trunc sigma function is_equiv equiv prod unit
+open eq is_trunc sigma function is_equiv equiv prod unit prod.ops
 
 /-
    We now prove that funext follows from a couple of weaker-looking forms

hott/init/types.hlean

@@ -66,10 +66,12 @@ definition pair := @prod.mk
 
 namespace prod
 
-  infixr * := prod
+  -- notation for n-ary tuples
+  notation `(` h `,` t:(foldl `,` (e r, prod.mk r e) h) `)` := t
   infixr × := prod
 
   namespace ops
+  infixr * := prod
   postfix `.1`:(max+1) := pr1
   postfix `.2`:(max+1) := pr2
   abbreviation pr₁ := @pr1
@@ -83,14 +85,10 @@ namespace prod
 
   end low_precedence_times
 
+  open prod.ops
+
   definition flip {A B : Type} (a : A × B) : B × A := pair (pr2 a) (pr1 a)
 
-  notation `pr₁` := pr1
-  notation `pr₂` := pr2
-
-  -- notation for n-ary tuples
-  notation `(` h `,` t:(foldl `,` (e r, prod.mk r e) h) `)` := t
-
   open well_founded
 
   section

hott/types/prod.hlean

@@ -9,7 +9,7 @@ Ported from Coq HoTT
 Theorems about products
 -/
 
-open eq equiv is_equiv is_trunc prod
+open eq equiv is_equiv is_trunc prod prod.ops
 
 variables {A A' B B' C D : Type}
           {a a' a'' : A} {b b₁ b₂ b' b'' : B} {u v w : A × B}

hott/types/sigma.hlean

@@ -277,7 +277,7 @@ namespace sigma
     begin intro uc, cases uc with u c, cases u, reflexivity end
     begin intro av, cases av with a v, cases v, reflexivity end)
 
-  open prod
+  open prod prod.ops
   definition assoc_equiv_prod (C : (A × A') → Type) : (Σa a', C (a,a')) ≃ (Σu, C u) :=
   equiv.mk _ (adjointify
     (λav, ⟨(av.1, av.2.1), av.2.2⟩)