diff --git a/hott/algebra/category/constructions/order.hlean b/hott/algebra/category/constructions/order.hlean
index ae77b9541..3e4ca2bf9 100644
--- a/hott/algebra/category/constructions/order.hlean
+++ b/hott/algebra/category/constructions/order.hlean
@@ -13,8 +13,8 @@ namespace category
 
 section
 universe variable l
-parameters (A : Type.{l}) [HA : is_hset A] [OA : weak_order.{l} A] 
-  [Hle : Π a b : A, is_hprop (a ≤ b)]
+parameters (A : Type.{l}) [HA : is_set A] [OA : weak_order.{l} A] 
+  [Hle : Π a b : A, is_prop (a ≤ b)]
 include A HA OA Hle
 
 definition precategory_order [constructor] : precategory.{l l} A :=
@@ -23,7 +23,7 @@ begin
   { intro a b, exact a ≤ b },
   { intro a b c, exact ge.trans },
   { intro a, apply le.refl },
-  do 5 (intros; apply is_hprop.elim),
+  do 5 (intros; apply is_prop.elim),
   { intros, apply is_trunc_succ }
 end
 
@@ -33,19 +33,11 @@ definition category_order : category.{l l} A :=
 begin
   fapply category.mk precategory_order,
   intros a b, fapply adjointify,
-  { intro f, apply le.antisymm, apply (iso.to_hom f), apply (iso.to_inv f) },
-  { intro f, fapply iso_eq, esimp[precategory_order], apply is_hprop.elim },
-  { intro p, apply is_hprop.elim }
+  { intro f, apply le.antisymm, apply iso.to_hom f, apply iso.to_inv f },
+  { intro f, fapply iso_eq, esimp[precategory_order], apply is_prop.elim },
+  { intro p, apply is_prop.elim }
 end
 
 end
 
-open fin
-
-definition category_fin [constructor] (n : nat) : category (fin n) :=
-category_order (fin n)
-
-definition Category_fin [reducible] [constructor] (n : nat) : Category :=
-Category.mk (fin n) (category_fin n)
-
 end category
diff --git a/hott/types/type_functor.hlean b/hott/types/type_functor.hlean
index 25d60ca2b..2e7465e23 100644
--- a/hott/types/type_functor.hlean
+++ b/hott/types/type_functor.hlean
@@ -9,7 +9,7 @@ More or less ported from Evan Cavallo's HoTT-Agda homotopy library.
 
 import types.pointed
 
-open equiv function pointed Pointed
+open equiv function pointed
 
 structure type_functor : Type :=
   (fun_ty : Type → Type)