From c64e5a114c0f540d545a9163abeda007fb9e4fce Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Mon, 15 Feb 2016 16:24:24 -0500
Subject: [PATCH] feat(circle): add missing facts that the circle is
 1-truncated and 0-connected

---
 hott/homotopy/circle.hlean | 21 +++++++++++++++++++--
 1 file changed, 19 insertions(+), 2 deletions(-)

diff --git a/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean
index 57841b5e80..5bdf06cfb3 100644
--- a/hott/homotopy/circle.hlean
+++ b/hott/homotopy/circle.hlean
@@ -8,9 +8,9 @@ Declaration of the circle
 
 import .sphere
 import types.bool types.int.hott types.equiv
-import algebra.homotopy_group algebra.hott
+import algebra.homotopy_group algebra.hott .connectedness
 
-open eq susp bool sphere_index is_equiv equiv equiv.ops is_trunc pi algebra
+open eq susp bool sphere_index is_equiv equiv equiv.ops is_trunc pi algebra homotopy
 
 definition circle : Type₀ := sphere 1
 
@@ -269,6 +269,23 @@ namespace circle
       induction H', reflexivity}
   end
 
+  definition is_trunc_circle [instance] : is_trunc 1 S¹ :=
+  begin
+    apply is_trunc_succ_of_is_trunc_loop,
+    { exact unit.star},
+    { intro x, apply is_trunc_equiv_closed_rev, apply eq_equiv_Z}
+  end
+
+  definition is_conn_circle [instance] : is_conn 0 S¹ :=
+  begin
+    fapply is_contr.mk,
+    { exact tr base},
+    { intro x, induction x with x,
+      induction x,
+      { reflexivity},
+      { apply is_prop.elimo}}
+  end
+
   definition circle_mul [reducible] (x y : S¹) : S¹ :=
   begin
     induction x,