From 052fbe0228980b0d4ead8b3350251b8028224fbe Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Fri, 24 Apr 2015 19:58:50 -0400
Subject: [PATCH] refactor(hott.init): remove subdirectories, merge some files

---
 hott/init/axioms/axioms.md                    |   6 -
 hott/init/axioms/funext_varieties.hlean       | 109 ------------------
 hott/init/bool.hlean                          |   2 +-
 hott/init/datatypes.hlean                     |  10 +-
 hott/init/default.hlean                       |   4 +-
 .../funext_of_ua.hlean => funext.hlean}       | 107 ++++++++++++++++-
 hott/init/init.md                             |   8 +-
 hott/init/logic.hlean                         |   2 +-
 hott/init/nat.hlean                           |   2 +-
 hott/init/trunc.hlean                         |   2 +-
 hott/init/{types/prod.hlean => types.hlean}   |  66 +++++++++--
 hott/init/types/empty.hlean                   |  23 ----
 hott/init/types/sigma.hlean                   |  26 -----
 hott/init/types/sum.hlean                     |  19 ---
 hott/init/types/types.md                      |   9 --
 hott/init/{axioms => }/ua.hlean               |   4 +-
 16 files changed, 176 insertions(+), 223 deletions(-)
 delete mode 100644 hott/init/axioms/axioms.md
 delete mode 100644 hott/init/axioms/funext_varieties.hlean
 rename hott/init/{axioms/funext_of_ua.hlean => funext.hlean} (58%)
 rename hott/init/{types/prod.hlean => types.hlean} (73%)
 delete mode 100644 hott/init/types/empty.hlean
 delete mode 100644 hott/init/types/sigma.hlean
 delete mode 100644 hott/init/types/sum.hlean
 delete mode 100644 hott/init/types/types.md
 rename hott/init/{axioms => }/ua.hlean (96%)

diff --git a/hott/init/axioms/axioms.md b/hott/init/axioms/axioms.md
deleted file mode 100644
index 6644bf5b3f..0000000000
--- a/hott/init/axioms/axioms.md
+++ /dev/null
@@ -1,6 +0,0 @@
-init.axioms
-===========
-
-* [ua](ua.hlean) : the univalence axiom
-* [funext_varieties](funext_varieties.hlean) : versions of function extensionality
-* [funext_of_ua](funext_of_ua.hlean) : univalence implies funext
diff --git a/hott/init/axioms/funext_varieties.hlean b/hott/init/axioms/funext_varieties.hlean
deleted file mode 100644
index 2d978d2dd5..0000000000
--- a/hott/init/axioms/funext_varieties.hlean
+++ /dev/null
@@ -1,109 +0,0 @@
-/-
-Copyright (c) 2014 Jakob von Raumer. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: init.axioms.funext_varieties
-Authors: Jakob von Raumer
-
-Ported from Coq HoTT
--/
-
-prelude
-import ..path ..trunc ..equiv
-
-open eq is_trunc sigma function
-
-/- In init.axioms.funext, we defined function extensionality to be the assertion
-   that the map apd10 is an equivalence.   We now prove that this follows
-   from a couple of weaker-looking forms of function extensionality.  We do
-   require eta conversion, which Coq 8.4+ has judgmentally.
-
-   This proof is originally due to Voevodsky; it has since been simplified
-   by Peter Lumsdaine and Michael Shulman. -/
-
-definition funext.{l k} :=
-  Π ⦃A : Type.{l}⦄ {P : A → Type.{k}} (f g : Π x, P x), is_equiv (@apd10 A P f g)
-
--- Naive funext is the simple assertion that pointwise equal functions are equal.
-definition naive_funext :=
-  Π ⦃A : Type⦄ {P : A → Type} (f g : Πx, P x), (f ∼ g) → f = g
-
--- Weak funext says that a product of contractible types is contractible.
-definition weak_funext :=
-  Π ⦃A : Type⦄ (P : A → Type) [H: Πx, is_contr (P x)], is_contr (Πx, P x)
-
-definition weak_funext_of_naive_funext : naive_funext → weak_funext :=
-  (λ nf A P (Pc : Πx, is_contr (P x)),
-    let c := λx, center (P x) in
-    is_contr.mk c (λ f,
-      have eq' : (λx, center (P x)) ∼ f,
-        from (λx, contr (f x)),
-      have eq : (λx, center (P x)) = f,
-        from nf A P (λx, center (P x)) f eq',
-      eq
-    )
-  )
-
-/- The less obvious direction is that WeakFunext implies Funext
-  (and hence all three are logically equivalent).  The point is that under weak
-  funext, the space of "pointwise homotopies" has the same universal property as
-  the space of paths. -/
-
-section
-  universe variables l k
-  parameters [wf : weak_funext.{l k}] {A : Type.{l}} {B : A → Type.{k}} (f : Π x, B x)
-
-  definition is_contr_sigma_homotopy [instance] : is_contr (Σ (g : Π x, B x), f ∼ g) :=
-    is_contr.mk (sigma.mk f (homotopy.refl f))
-      (λ dp, sigma.rec_on dp
-        (λ (g : Π x, B x) (h : f ∼ g),
-          let r := λ (k : Π x, Σ y, f x = y),
-            @sigma.mk _ (λg, f ∼ g)
-              (λx, pr1 (k x)) (λx, pr2 (k x)) in
-          let s := λ g h x, @sigma.mk _ (λy, f x = y) (g x) (h x) in
-          have t1 : Πx, is_contr (Σ y, f x = y),
-            from (λx, !is_contr_sigma_eq),
-          have t2 : is_contr (Πx, Σ y, f x = y),
-            from !wf,
-          have t3 : (λ x, @sigma.mk _ (λ y, f x = y) (f x) idp) = s g h,
-            from @eq_of_is_contr (Π x, Σ y, f x = y) t2 _ _,
-          have t4 : r (λ x, sigma.mk (f x) idp) = r (s g h),
-            from ap r t3,
-          have endt : sigma.mk f (homotopy.refl f) = sigma.mk g h,
-            from t4,
-          endt
-        )
-      )
-
-  parameters (Q : Π g (h : f ∼ g), Type) (d : Q f (homotopy.refl f))
-
-  definition homotopy_ind (g : Πx, B x) (h : f ∼ g) : Q g h :=
-    @transport _ (λ gh, Q (pr1 gh) (pr2 gh)) (sigma.mk f (homotopy.refl f)) (sigma.mk g h)
-      (@eq_of_is_contr _ is_contr_sigma_homotopy _ _) d
-
-  local attribute weak_funext [reducible]
-  local attribute homotopy_ind [reducible]
-  definition homotopy_ind_comp : homotopy_ind f (homotopy.refl f) = d :=
-    (@hprop_eq_of_is_contr _ _ _ _ !eq_of_is_contr idp)⁻¹ ▹ idp
-end
-
--- Now the proof is fairly easy; we can just use the same induction principle on both sides.
-universe variables l k
-
-local attribute weak_funext [reducible]
-theorem funext_of_weak_funext (wf : weak_funext.{l k}) : funext.{l k} :=
-  λ A B f g,
-    let eq_to_f := (λ g' x, f = g') in
-    let sim2path := homotopy_ind f eq_to_f idp in
-    assert t1 : sim2path f (homotopy.refl f) = idp,
-      proof homotopy_ind_comp f eq_to_f idp qed,
-    assert t2 : apd10 (sim2path f (homotopy.refl f)) = (homotopy.refl f),
-      proof ap apd10 t1 qed,
-    have sect : apd10 ∘ (sim2path g) ∼ id,
-      proof (homotopy_ind f (λ g' x, apd10 (sim2path g' x) = x) t2) g qed,
-    have retr : (sim2path g) ∘ apd10 ∼ id,
-      from (λ h, eq.rec_on h (homotopy_ind_comp f _ idp)),
-    is_equiv.adjointify apd10 (sim2path g) sect retr
-
-definition funext_from_naive_funext : naive_funext -> funext :=
-  compose funext_of_weak_funext weak_funext_of_naive_funext
diff --git a/hott/init/bool.hlean b/hott/init/bool.hlean
index 6c4e05bed4..0d066cf6e1 100644
--- a/hott/init/bool.hlean
+++ b/hott/init/bool.hlean
@@ -7,7 +7,7 @@ Authors: Leonardo de Moura
 -/
 
 prelude
-import init.datatypes init.reserved_notation
+import init.reserved_notation
 
 namespace bool
   definition cond {A : Type} (b : bool) (t e : A) :=
diff --git a/hott/init/datatypes.hlean b/hott/init/datatypes.hlean
index 124b89ec39..80a25c2914 100644
--- a/hott/init/datatypes.hlean
+++ b/hott/init/datatypes.hlean
@@ -19,12 +19,6 @@ notation `Type₃` := Type.{3}
 inductive unit.{l} : Type.{l} :=
 star : unit
 
-namespace unit
-
-  notation `⋆` := star
-
-end unit
-
 inductive empty.{l} : Type.{l}
 
 inductive eq.{l} {A : Type.{l}} (a : A) : A → Type.{l} :=
@@ -46,6 +40,9 @@ sum.inl a
 definition sum.intro_right [reducible] (A : Type) {B : Type} (b : B) : sum A B :=
 sum.inr b
 
+structure sigma {A : Type} (B : A → Type) :=
+mk :: (pr1 : A) (pr2 : B pr1)
+
 -- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26.
 -- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))).
 -- This representation can be coerced in whatever we want (e.g., naturals, integers, reals, etc).
@@ -63,7 +60,6 @@ inductive num : Type :=
 | zero  : num
 | pos   : pos_num → num
 
-
 namespace num
   open pos_num
   definition succ (a : num) : num :=
diff --git a/hott/init/default.hlean b/hott/init/default.hlean
index 56397d75ec..148169c407 100644
--- a/hott/init/default.hlean
+++ b/hott/init/default.hlean
@@ -9,7 +9,7 @@ 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 init.types.empty
+import init.types
 import init.trunc init.path init.equiv init.util
-import init.axioms.ua init.axioms.funext_of_ua
+import init.ua init.funext
 import init.hedberg init.nat init.hit
diff --git a/hott/init/axioms/funext_of_ua.hlean b/hott/init/funext.hlean
similarity index 58%
rename from hott/init/axioms/funext_of_ua.hlean
rename to hott/init/funext.hlean
index 6a20264b4f..4af286bd74 100644
--- a/hott/init/axioms/funext_of_ua.hlean
+++ b/hott/init/funext.hlean
@@ -2,17 +2,114 @@
 Copyright (c) 2014 Jakob von Raumer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
-Module: init.axioms.funext_of_ua
-Author: Jakob von Raumer
+Module: init.funext
+Authors: Jakob von Raumer
 
 Ported from Coq HoTT
 -/
 
 prelude
-import ..equiv ..datatypes ..types.prod
-import .funext_varieties .ua
+import .trunc .equiv .ua
+open eq is_trunc sigma function is_equiv equiv prod unit
 
-open eq function prod is_trunc sigma equiv is_equiv unit
+/-
+   We now prove that funext follows from a couple of weaker-looking forms
+   of function extensionality.
+
+   This proof is originally due to Voevodsky; it has since been simplified
+   by Peter Lumsdaine and Michael Shulman.
+-/
+
+definition funext.{l k} :=
+  Π ⦃A : Type.{l}⦄ {P : A → Type.{k}} (f g : Π x, P x), is_equiv (@apd10 A P f g)
+
+-- Naive funext is the simple assertion that pointwise equal functions are equal.
+definition naive_funext :=
+  Π ⦃A : Type⦄ {P : A → Type} (f g : Πx, P x), (f ∼ g) → f = g
+
+-- Weak funext says that a product of contractible types is contractible.
+definition weak_funext :=
+  Π ⦃A : Type⦄ (P : A → Type) [H: Πx, is_contr (P x)], is_contr (Πx, P x)
+
+definition weak_funext_of_naive_funext : naive_funext → weak_funext :=
+  (λ nf A P (Pc : Πx, is_contr (P x)),
+    let c := λx, center (P x) in
+    is_contr.mk c (λ f,
+      have eq' : (λx, center (P x)) ∼ f,
+        from (λx, contr (f x)),
+      have eq : (λx, center (P x)) = f,
+        from nf A P (λx, center (P x)) f eq',
+      eq
+    )
+  )
+
+/-
+  The less obvious direction is that weak_funext implies funext
+  (and hence all three are logically equivalent).  The point is that under weak
+  funext, the space of "pointwise homotopies" has the same universal property as
+  the space of paths.
+-/
+
+section
+  universe variables l k
+  parameters [wf : weak_funext.{l k}] {A : Type.{l}} {B : A → Type.{k}} (f : Π x, B x)
+
+  definition is_contr_sigma_homotopy [instance] : is_contr (Σ (g : Π x, B x), f ∼ g) :=
+    is_contr.mk (sigma.mk f (homotopy.refl f))
+      (λ dp, sigma.rec_on dp
+        (λ (g : Π x, B x) (h : f ∼ g),
+          let r := λ (k : Π x, Σ y, f x = y),
+            @sigma.mk _ (λg, f ∼ g)
+              (λx, pr1 (k x)) (λx, pr2 (k x)) in
+          let s := λ g h x, @sigma.mk _ (λy, f x = y) (g x) (h x) in
+          have t1 : Πx, is_contr (Σ y, f x = y),
+            from (λx, !is_contr_sigma_eq),
+          have t2 : is_contr (Πx, Σ y, f x = y),
+            from !wf,
+          have t3 : (λ x, @sigma.mk _ (λ y, f x = y) (f x) idp) = s g h,
+            from @eq_of_is_contr (Π x, Σ y, f x = y) t2 _ _,
+          have t4 : r (λ x, sigma.mk (f x) idp) = r (s g h),
+            from ap r t3,
+          have endt : sigma.mk f (homotopy.refl f) = sigma.mk g h,
+            from t4,
+          endt
+        )
+      )
+
+  parameters (Q : Π g (h : f ∼ g), Type) (d : Q f (homotopy.refl f))
+
+  definition homotopy_ind (g : Πx, B x) (h : f ∼ g) : Q g h :=
+    @transport _ (λ gh, Q (pr1 gh) (pr2 gh)) (sigma.mk f (homotopy.refl f)) (sigma.mk g h)
+      (@eq_of_is_contr _ is_contr_sigma_homotopy _ _) d
+
+  local attribute weak_funext [reducible]
+  local attribute homotopy_ind [reducible]
+  definition homotopy_ind_comp : homotopy_ind f (homotopy.refl f) = d :=
+    (@hprop_eq_of_is_contr _ _ _ _ !eq_of_is_contr idp)⁻¹ ▹ idp
+end
+
+/- Now the proof is fairly easy; we can just use the same induction principle on both sides. -/
+section
+universe variables l k
+
+local attribute weak_funext [reducible]
+theorem funext_of_weak_funext (wf : weak_funext.{l k}) : funext.{l k} :=
+  λ A B f g,
+    let eq_to_f := (λ g' x, f = g') in
+    let sim2path := homotopy_ind f eq_to_f idp in
+    assert t1 : sim2path f (homotopy.refl f) = idp,
+      proof homotopy_ind_comp f eq_to_f idp qed,
+    assert t2 : apd10 (sim2path f (homotopy.refl f)) = (homotopy.refl f),
+      proof ap apd10 t1 qed,
+    have sect : apd10 ∘ (sim2path g) ∼ id,
+      proof (homotopy_ind f (λ g' x, apd10 (sim2path g' x) = x) t2) g qed,
+    have retr : (sim2path g) ∘ apd10 ∼ id,
+      from (λ h, eq.rec_on h (homotopy_ind_comp f _ idp)),
+    is_equiv.adjointify apd10 (sim2path g) sect retr
+
+definition funext_from_naive_funext : naive_funext → funext :=
+  compose funext_of_weak_funext weak_funext_of_naive_funext
+end
 
 section
   universe variables l
diff --git a/hott/init/init.md b/hott/init/init.md
index 1956fc274e..bb5912de7a 100644
--- a/hott/init/init.md
+++ b/hott/init/init.md
@@ -13,13 +13,13 @@ Syntax declarations:
 
 Datatypes and logic:
 
-* [datatypes](datatypes.hlean)
 * [logic](logic.hlean)
+* [datatypes](datatypes.hlean) (declaration of common types)
 * [bool](bool.hlean)
 * [num](num.hlean)
 * [nat](nat.hlean)
 * [function](function.hlean)
-* [types](types/types.md) (subfolder)
+* [types](types.hlean) (notation and some theorems for the remaining basic types)
 
 HoTT basics:
 
@@ -27,7 +27,8 @@ HoTT basics:
 * [hedberg](hedberg.hlean)
 * [trunc](trunc.hlean)
 * [equiv](equiv.hlean)
-* [axioms](axioms/axioms.md) (subfolder)
+* [ua](ua.hlean) (declaration of the univalence axiom, and some basic properties)
+* [funext](funext.hlean) (proof of equivalence of certain notions of function exensionality, and a proof that function extensionality follows from univalence)
 
 Support for well-founded recursion and automation:
 
@@ -38,4 +39,3 @@ Support for well-founded recursion and automation:
 The default import:
 
 * [default](default.hlean)
-
diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean
index 348fdc4f5d..377e821b85 100644
--- a/hott/init/logic.hlean
+++ b/hott/init/logic.hlean
@@ -7,7 +7,7 @@ Authors: Leonardo de Moura
 -/
 
 prelude
-import init.datatypes init.reserved_notation
+import init.reserved_notation
 
 definition not.{l} (a : Type.{l}) := a → empty.{l}
 prefix `¬` := not
diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean
index 8c2fbd57d9..495cc4d4dd 100644
--- a/hott/init/nat.hlean
+++ b/hott/init/nat.hlean
@@ -7,7 +7,7 @@ Authors: Floris van Doorn, Leonardo de Moura
 -/
 
 prelude
-import init.wf init.tactic init.hedberg init.util init.types.sum
+import init.wf init.tactic init.hedberg init.util init.types
 
 open eq.ops decidable sum
 
diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean
index e26ee1ca53..87c9fd9cd7 100644
--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@@ -11,7 +11,7 @@ TODO: can we replace some definitions with a hprop as codomain by theorems?
 -/
 
 prelude
-import .logic .equiv .types.empty .types.sigma
+import .logic .equiv .types
 open eq nat sigma unit
 
 namespace is_trunc
diff --git a/hott/init/types/prod.hlean b/hott/init/types.hlean
similarity index 73%
rename from hott/init/types/prod.hlean
rename to hott/init/types.hlean
index be336c4e66..6e31615c77 100644
--- a/hott/init/types/prod.hlean
+++ b/hott/init/types.hlean
@@ -1,20 +1,73 @@
 /-
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Copyright (c) 2014-2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
-Module: init.types.prod
-Author: Leonardo de Moura, Jeremy Avigad
+Module: init.types
+Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn, Jakob von Raumer
 -/
 
 prelude
-import ..wf ..num
+import .logic .num .wf
+
+-- Empty type
+-- ----------
+
+namespace empty
+
+  protected theorem elim (A : Type) (H : empty) : A :=
+  empty.rec (λe, A) H
+
+end empty
+
+protected definition empty.has_decidable_eq [instance] : decidable_eq empty :=
+take (a b : empty), decidable.inl (!empty.elim a)
+
+-- Unit type
+-- ---------
+
+namespace unit
+
+  notation `⋆` := star
+
+end unit
+
+-- Sigma type
+-- ----------
+
+notation `Σ` binders `,` r:(scoped P, sigma P) := r
+
+namespace sigma
+  notation `⟨`:max t:(foldr `,` (e r, mk e r)) `⟩`:0 := t --input ⟨ ⟩ as \< \>
+
+  namespace ops
+  postfix `.1`:(max+1) := pr1
+  postfix `.2`:(max+1) := pr2
+  abbreviation pr₁ := @pr1
+  abbreviation pr₂ := @pr2
+  end ops
+end sigma
+
+-- Sum type
+-- --------
+
+namespace sum
+  infixr ⊎ := sum
+  infixr + := sum
+  namespace low_precedence_plus
+    reserve infixr `+`:25  -- conflicts with notation for addition
+    infixr `+` := sum
+  end low_precedence_plus
+end sum
+
+-- Product type
+-- ------------
 
 definition pair := @prod.mk
 
 namespace prod
 
-  notation A * B := prod A B
-  notation A × B := prod A B
+  infixr * := prod
+  infixr × := prod
 
   namespace ops
   postfix `.1`:(max+1) := pr1
@@ -30,7 +83,6 @@ namespace 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
diff --git a/hott/init/types/empty.hlean b/hott/init/types/empty.hlean
deleted file mode 100644
index f9f221b519..0000000000
--- a/hott/init/types/empty.hlean
+++ /dev/null
@@ -1,23 +0,0 @@
-/-
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: init.types.empty
-Author: Jeremy Avigad, Floris van Doorn, Jakob von Raumer
--/
-
-prelude
-import ..datatypes ..logic
-
--- Empty type
--- ----------
-
-namespace empty
-
-  protected theorem elim (A : Type) (H : empty) : A :=
-  empty.rec (λe, A) H
-
-end empty
-
-protected definition empty.has_decidable_eq [instance] : decidable_eq empty :=
-take (a b : empty), decidable.inl (!empty.elim a)
diff --git a/hott/init/types/sigma.hlean b/hott/init/types/sigma.hlean
deleted file mode 100644
index 53d2600ab4..0000000000
--- a/hott/init/types/sigma.hlean
+++ /dev/null
@@ -1,26 +0,0 @@
-/-
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: init.types.sigma
-Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
--/
-
-prelude
-import init.num
-
-structure sigma {A : Type} (B : A → Type) :=
-mk :: (pr1 : A) (pr2 : B pr1)
-
-notation `Σ` binders `,` r:(scoped P, sigma P) := r
-
-namespace sigma
-  notation `⟨`:max t:(foldr `,` (e r, mk e r)) `⟩`:0 := t --input ⟨ ⟩ as \< \>
-
-  namespace ops
-  postfix `.1`:(max+1) := pr1
-  postfix `.2`:(max+1) := pr2
-  abbreviation pr₁ := @pr1
-  abbreviation pr₂ := @pr2
-  end ops
-end sigma
diff --git a/hott/init/types/sum.hlean b/hott/init/types/sum.hlean
deleted file mode 100644
index 231aacada2..0000000000
--- a/hott/init/types/sum.hlean
+++ /dev/null
@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: init.types.sum
-Author: Leonardo de Moura, Jeremy Avigad
--/
-
-prelude
-import init.datatypes init.reserved_notation
-
-namespace sum
-  notation A ⊎ B := sum A B
-  notation A + B := sum A B
-  namespace low_precedence_plus
-    reserve infixr `+`:25  -- conflicts with notation for addition
-    infixr `+` := sum
-  end low_precedence_plus
-end sum
diff --git a/hott/init/types/types.md b/hott/init/types/types.md
deleted file mode 100644
index 019ef23c9c..0000000000
--- a/hott/init/types/types.md
+++ /dev/null
@@ -1,9 +0,0 @@
-init.types
-==========
-
-Some basic datatypes.
-
-* [empty](empty.hlean)
-* [prod](prod.hlean)
-* [sigma](sigma.hlean)
-* [sum](sum.hlean)
\ No newline at end of file
diff --git a/hott/init/axioms/ua.hlean b/hott/init/ua.hlean
similarity index 96%
rename from hott/init/axioms/ua.hlean
rename to hott/init/ua.hlean
index 8f5a2f20f6..e7d9f5139b 100644
--- a/hott/init/axioms/ua.hlean
+++ b/hott/init/ua.hlean
@@ -2,14 +2,14 @@
 Copyright (c) 2014 Jakob von Raumer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
-Module: init.axioms.ua
+Module: init.ua
 Author: Jakob von Raumer
 
 Ported from Coq HoTT
 -/
 
 prelude
-import ..path ..equiv
+import .equiv
 open eq equiv is_equiv
 
 --Ensure that the types compared are in the same universe