From cc2de8a8d940acb47d80da9b0dda6472c5875171 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Wed, 3 Dec 2014 01:54:05 -0500
Subject: [PATCH] feat(library/hott): complete proof that object types of
 proper hott categories are one truncated

---
 library/hott/algebra/category/basic.lean | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/library/hott/algebra/category/basic.lean b/library/hott/algebra/category/basic.lean
index 25cee9a811..1056db316f 100644
--- a/library/hott/algebra/category/basic.lean
+++ b/library/hott/algebra/category/basic.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Jakob von Raumer
 
-import ..precategory.basic ..precategory.morphism
+import ..precategory.basic ..precategory.morphism ..precategory.iso
 import hott.equiv hott.trunc
 
 open precategory morphism is_equiv path truncation nat sigma sigma.ops
@@ -24,15 +24,13 @@ namespace category
   definition path_of_iso {a b : ob} : a ≅ b → a ≈ b :=
   iso_of_path⁻¹
 
-  definition foo {a b : ob} :
-
-  definition ob_1_type : is_trunc -2 .+1 .+1 .+1 ob :=
+  definition ob_1_type : is_trunc nat.zero .+1 ob :=
   begin
     apply is_trunc_succ, intros (a, b),
-    /-fapply trunc_equiv,
-      exact (@path_of_iso ob C a b),
-      apply inv_closed,
-    exact sorry,-/
+    fapply trunc_equiv,
+          exact (@path_of_iso _ _ a b),
+        apply inv_closed,
+    apply is_hset_iso,
   end
 
 end category