diff --git a/library/hott/algebra/category/basic.lean b/library/hott/algebra/category/basic.lean
new file mode 100644
index 0000000000..49bed947e6
--- /dev/null
+++ b/library/hott/algebra/category/basic.lean
@@ -0,0 +1,32 @@
+-- Copyright (c) 2014 Jakob von Raumer. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Jakob von Raumer
+
+import ..precategory.basic ..precategory.morphism
+import hott.equiv hott.trunc
+
+open precategory morphism is_equiv path truncation nat sigma sigma.ops
+
+-- A category is a precategory extended by a witness,
+-- that the function assigning to each isomorphism a path,
+-- is an equivalecnce.
+structure category [class] (ob : Type) extends (precategory ob) :=
+  (iso_of_path_equiv : Π {a b : ob}, is_equiv (@iso_of_path ob (precategory.mk hom _ comp ID assoc id_left id_right) a b))
+
+namespace category
+  variables {ob : Type} (C : category ob) {a b : ob}
+  include C
+
+  -- Make iso_of_path_equiv a class instance
+  -- TODO: Unsafe class instance?
+  instance [persistent] iso_of_path_equiv
+
+  definition path_of_iso {a b : ob} : (Σ (f : hom a b), is_iso f) → a ≈ b :=
+  iso_of_path⁻¹
+
+  definition ob_1_type : is_trunc 1 ob := sorry
+
+end category
+
+-- Bundled version of categories
+inductive Category : Type := mk : Π (ob : Type), category ob → Category