From 9d919573035b4093f450149a9815ffc06a289b27 Mon Sep 17 00:00:00 2001
From: Ulrik Buchholtz <ulrikbuchholtz@gmail.com>
Date: Sat, 27 Jan 2018 19:42:09 +0100
Subject: [PATCH] connectivity of loop_susp_counit

---
 homotopy/susp.hlean | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/homotopy/susp.hlean b/homotopy/susp.hlean
index 6a9c682..73c8b19 100644
--- a/homotopy/susp.hlean
+++ b/homotopy/susp.hlean
@@ -164,10 +164,22 @@ sorry
 
     include HA
 
+    open is_conn trunc_index
+
     -- connectivity of loop_susp_counit
     definition is_conn_fun_loop_susp_counit {k : ℕ} (H : k ≤ 2 * n)
       : is_conn_fun k (loop_susp_counit A) :=
-    λ a, sorry
+    begin
+      intro a, apply is_conn.is_conn_equiv_closed_rev k (fiber_loop_susp_counit_equiv a),
+      fapply @is_conn.is_conn_of_le (fiber prod_of_wedge (a, a)) k (2 * n)
+        (of_nat_le_of_nat H),
+      assert H : of_nat (2 * n) = of_nat n + of_nat n,
+      { rewrite (of_nat_add_of_nat n n), apply ap of_nat,
+        apply trans (nat.mul_comm 2 n),
+        apply ap (λ k, k + n), exact nat.zero_add n },
+      rewrite H,
+      exact is_conn_fun_prod_of_wedge n n (a, a)
+    end
   end
 
 end susp