diff --git a/hott/algebra/algebra.md b/hott/algebra/algebra.md
index 18bd38464..d0fc3578a 100644
--- a/hott/algebra/algebra.md
+++ b/hott/algebra/algebra.md
@@ -1,16 +1,24 @@
 algebra
 =======
 
-Note: most of these files are ported from the standard library. If anything needs to be changed, it is probably a good idea to change it in the standard library and then port the file again (see also [script/port.pl](../../script/port.pl)).
+The following files are ported from the standard library. If anything needs to be changed, it is probably a good idea to change it in the standard library and then port the file again (see also [script/port.pl](../../script/port.pl)).
 
 * [binary](binary.hlean) : properties of binary operations
 * [relation](relation.hlean) : properties of relations
 * [group](group.hlean)
 * [ring](ring.hlean)
+* [order](order.hlean)
 * [ordered_group](ordered_group.hlean)
 * [ordered_ring](ordered_ring.hlean)
 * [field](field.hlean)
 
+Files which are not ported:
+
+* [hott](hott.hlean) : Basic theorems about the algebraic hierarchy specific to HoTT
+* [trunc_group](trunc_group.hlean) : truncate an infinity-group to a group
+* [homotopy_group](homotopy_group.hlean) : homotopy groups of a pointed type
+* [e_closure](e_closure.hlean) : the type of words formed by a relation
+
 Subfolders:
 
 * [category](category/category.md) : Category Theory
diff --git a/hott/hit/trunc.hlean b/hott/hit/trunc.hlean
index 68278b7ef..6404c2d53 100644
--- a/hott/hit/trunc.hlean
+++ b/hott/hit/trunc.hlean
@@ -104,13 +104,13 @@ namespace trunc
   /- Propositional truncation -/
 
   -- should this live in hprop?
-  definition merely [reducible] (A : Type) : Type := trunc -1 A
+  definition merely [reducible] (A : Type) : hprop := trunctype.mk (trunc -1 A) _
 
   notation `||`:max A `||`:0 := merely A
   notation `∥`:max A `∥`:0   := merely A
 
-  definition Exists [reducible] (P : X → Type) : Type := ∥ sigma P ∥
-  definition or [reducible] (A B : Type) : Type := ∥ A ⊎ B ∥
+  definition Exists [reducible] (P : X → Type) : hprop := ∥ sigma P ∥
+  definition or [reducible] (A B : Type) : hprop := ∥ A ⊎ B ∥
 
   notation `exists` binders `,` r:(scoped P, Exists P) := r
   notation `∃` binders `,` r:(scoped P, Exists P) := r
diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean
index 099e92d5f..db4d15867 100644
--- a/hott/types/pointed.hlean
+++ b/hott/types/pointed.hlean
@@ -352,4 +352,8 @@ namespace pointed
   definition equiv_of_pequiv [constructor] (f : A ≃* B) : A ≃ B :=
   equiv.mk f _
 
+  definition pua {A B : Type*} (f : A ≃* B) : A = B :=
+  Pointed_eq (equiv_of_pequiv f) !respect_pt
+
+
 end pointed
diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean
index beaa30ea2..a77beda18 100644
--- a/hott/types/sigma.hlean
+++ b/hott/types/sigma.hlean
@@ -413,11 +413,11 @@ namespace sigma
   notation [parsing_only] `{` binder `|` r:(scoped:1 P, subtype P) `}` := r
 
   /- To prove equality in a subtype, we only need equality of the first component. -/
-  definition subtype_eq [H : Πa, is_hprop (B a)] (u v : {a | B a}) : u.1 = v.1 → u = v :=
+  definition subtype_eq [H : Πa, is_hprop (B a)] {u v : {a | B a}} : u.1 = v.1 → u = v :=
   sigma_eq_unc ∘ inv pr1
 
   definition is_equiv_subtype_eq [H : Πa, is_hprop (B a)] (u v : {a | B a})
-      : is_equiv (subtype_eq u v) :=
+      : is_equiv (subtype_eq : u.1 = v.1 → u = v) :=
   !is_equiv_compose
   local attribute is_equiv_subtype_eq [instance]
 
@@ -426,14 +426,13 @@ namespace sigma
 
   definition subtype_eq_inv {A : Type} {B : A → Type} [H : Πa, is_hprop (B a)] (u v : Σa, B a)
     : u = v → u.1 = v.1 :=
-  (subtype_eq u v)⁻¹ᶠ
+  subtype_eq⁻¹ᶠ
 
   local attribute subtype_eq_inv [reducible]
   definition is_equiv_subtype_eq_inv {A : Type} {B : A → Type} [H : Πa, is_hprop (B a)]
     (u v : Σa, B a) : is_equiv (subtype_eq_inv u v) :=
   _
 
-
   /- truncatedness -/
   theorem is_trunc_sigma (B : A → Type) (n : trunc_index)
       [HA : is_trunc n A] [HB : Πa, is_trunc n (B a)] : is_trunc n (Σa, B a) :=
@@ -447,6 +446,11 @@ namespace sigma
       exact IH _ _ _ _}
   end
 
+  theorem is_trunc_subtype (B : A → hprop) (n : trunc_index)
+      [HA : is_trunc (n.+1) A] : is_trunc (n.+1) (Σa, B a) :=
+  @(is_trunc_sigma B (n.+1)) _ (λa, !is_trunc_succ_of_is_hprop)
+
 end sigma
 
 attribute sigma.is_trunc_sigma [instance] [priority 1490]
+attribute sigma.is_trunc_subtype [instance] [priority 1200]
diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean
index c239b5974..f3212cac3 100644
--- a/hott/types/trunc.hlean
+++ b/hott/types/trunc.hlean
@@ -241,6 +241,8 @@ namespace trunc
     : transport (λa, trunc n (P a)) p (tr x) = tr (p ▸ x) :=
   by induction p; reflexivity
 
+  definition image {A B : Type} (f : A → B) (b : B) : hprop := ∃(a : A), f a = b
+
 end trunc open trunc
 
 namespace function