From 71cffd29a0e32a8a2b4825ed23710989eb2adbcc Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Tue, 16 Dec 2014 15:10:12 -0500
Subject: [PATCH] chore(hott) minor corrections

---
 hott/equiv_precomp.hlean                | 2 +-
 hott/init/axioms/funext_from_ua.hlean   | 2 +-
 hott/init/axioms/funext_varieties.hlean | 1 +
 hott/init/default.hlean                 | 6 +++---
 hott/init/function.hlean                | 4 ++--
 hott/init/types/empty.hlean             | 3 +++
 hott/init/types/prod.hlean              | 6 +++++-
 7 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/hott/equiv_precomp.hlean b/hott/equiv_precomp.hlean
index 81c44c97f1..067dae56f9 100644
--- a/hott/equiv_precomp.hlean
+++ b/hott/equiv_precomp.hlean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Jakob von Raumer
 -- Ported from Coq HoTT
-import init.equiv init.axioms.funext
+
 open eq function funext
 
 namespace is_equiv
diff --git a/hott/init/axioms/funext_from_ua.hlean b/hott/init/axioms/funext_from_ua.hlean
index 46083b6a08..89a9fddac6 100644
--- a/hott/init/axioms/funext_from_ua.hlean
+++ b/hott/init/axioms/funext_from_ua.hlean
@@ -3,7 +3,7 @@
 -- Author: Jakob von Raumer
 -- Ported from Coq HoTT
 prelude
-import ..equiv ..datatypes
+import ..equiv ..datatypes ..types.prod
 import .funext_varieties .ua .funext
 
 open eq function prod sigma truncation equiv is_equiv unit ua_type
diff --git a/hott/init/axioms/funext_varieties.hlean b/hott/init/axioms/funext_varieties.hlean
index a100693f9f..227d9cfb68 100644
--- a/hott/init/axioms/funext_varieties.hlean
+++ b/hott/init/axioms/funext_varieties.hlean
@@ -2,6 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Jakob von Raumer
 -- Ported from Coq HoTT
+prelude
 import ..path ..trunc ..equiv .funext
 
 open eq truncation sigma function
diff --git a/hott/init/default.hlean b/hott/init/default.hlean
index 3f5356ddc2..024335b332 100644
--- a/hott/init/default.hlean
+++ b/hott/init/default.hlean
@@ -2,11 +2,11 @@
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
-Authors: Leonardo de Moura
+Authors: Leonardo de Moura, Jakob von Raumer
 -/
 prelude
 import init.datatypes init.reserved_notation init.tactic init.logic
 import init.bool init.num init.priority init.relation init.wf
-import init.types.sigma init.types.prod
+import init.types.sigma init.types.prod init.types.empty
 import init.trunc init.path init.equiv
-import init.axioms.funext
+import init.axioms.ua init.axioms.funext init.axioms.funext_from_ua
diff --git a/hott/init/function.hlean b/hott/init/function.hlean
index d758d3b264..eb2af4e3df 100644
--- a/hott/init/function.hlean
+++ b/hott/init/function.hlean
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 General operations on functions.
 -/
 prelude
+import init.reserved_notation
 
 namespace function
 
@@ -36,7 +37,6 @@ definition flip {A : Type} {B : Type} {C : A → B → Type} (f : Πx y, C x y)
 definition app {A : Type} {B : A → Type} (f : Πx, B x) (x : A) : B x :=
 f x
 
-precedence `∘`:60
 precedence `∘'`:60
 precedence `on`:1
 precedence `$`:1
@@ -44,7 +44,7 @@ precedence `$`:1
 variables {f g : A → B}
 
 
-infixr  ∘                 := compose
+infixr  ∘                  := compose
 infixr  ∘'                 := dcompose
 infixl  on                 := on_fun
 infixr  $                  := app
diff --git a/hott/init/types/empty.hlean b/hott/init/types/empty.hlean
index ef96e63626..fea08e5b51 100644
--- a/hott/init/types/empty.hlean
+++ b/hott/init/types/empty.hlean
@@ -4,12 +4,15 @@
 
 prelude
 import ..datatypes ..logic
+
 -- Empty type
 -- ----------
 
 namespace empty
+
   protected theorem elim (A : Type) (H : empty) : A :=
   rec (λe, A) H
+
 end empty
 
 protected definition empty.has_decidable_eq [instance] : decidable_eq empty :=
diff --git a/hott/init/types/prod.hlean b/hott/init/types/prod.hlean
index e9cb0fa876..a9e99c5cf7 100644
--- a/hott/init/types/prod.hlean
+++ b/hott/init/types/prod.hlean
@@ -2,7 +2,6 @@
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
-Module: data.prod.decl
 Author: Leonardo de Moura, Jeremy Avigad
 -/
 prelude
@@ -11,13 +10,18 @@ import ..wf
 definition pair := @prod.mk
 
 namespace prod
+
   notation A * B := prod A B
   notation A × B := prod A B
+
   namespace low_precedence_times
+
     reserve infixr `*`:30  -- conflicts with notation for multiplication
     infixr `*` := prod
+
   end low_precedence_times
 
+  -- TODO: add lemmas about flip to /hott/types/prod.hlean
   definition flip {A B : Type} (a : A × B) : B × A := pair (pr2 a) (pr1 a)
 
   notation `pr₁` := pr1