From d7b853071883bad744e9ccec217e0038f705fdae Mon Sep 17 00:00:00 2001
From: Ulrik Buchholtz <ulrikbuchholtz@gmail.com>
Date: Sun, 21 Jan 2018 12:28:43 +0100
Subject: [PATCH] prove that [n;k]Grp is an (n+1)-type

---
 higher_groups.hlean | 19 ++++++++++++++++++-
 move_to_lib.hlean   | 13 +++++++++++++
 2 files changed, 31 insertions(+), 1 deletion(-)

diff --git a/higher_groups.hlean b/higher_groups.hlean
index 5b7e709..4765edf 100644
--- a/higher_groups.hlean
+++ b/higher_groups.hlean
@@ -6,7 +6,7 @@ Authors: Ulrik Buchholtz, Egbert Rijke, Floris van Doorn
 Formalization of the higher groups paper
 -/
 
-import .move_to_lib
+import .pointed_pi
 open eq is_conn pointed is_trunc trunc equiv is_equiv trunc_index susp nat algebra
      prod.ops sigma sigma.ops
 namespace higher_group
@@ -240,4 +240,21 @@ definition ωStabilize (G : [n;k]Grp) : [n;ω]Grp :=
 
 /- to do: adjunction (and ωStabilize ∘ ωForget =?= id) -/
 
+definition is_trunc_Grp (n k : ℕ) : is_trunc (n + 1) [n;k]Grp :=
+begin
+  apply @is_trunc_equiv_closed_rev _ _ (n + 1) (Grp_equiv n k),
+  apply is_trunc_succ_intro, intros X Y,
+  apply @is_trunc_equiv_closed_rev _ _ _ (ptruncconntype_eq_equiv X Y),
+  apply @is_trunc_equiv_closed_rev _ _ _ (pequiv.sigma_char_equiv' X Y),
+  apply @is_trunc_subtype (X →* Y) (λ f, trunctype.mk' -1 (is_equiv f)),
+  apply is_trunc_pmap_of_is_conn X k.-2 (n + 1).-2 (n + k) Y,
+  { clear X Y, induction k with k IH,
+    { induction n with n IH,
+      { apply le.refl },
+      { exact trunc_index.succ_le_succ IH } },
+    { rewrite (trunc_index.succ_add_plus_two (nat.succ k).-2 (n + 1).-2),
+      exact trunc_index.succ_le_succ IH } },
+  { exact _ }
+end
+
 end higher_group
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index d1e8b82..3e0b04e 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -620,6 +620,19 @@ begin
     refine !idp_con ⬝ _, reflexivity },
 end
 
+definition pequiv.sigma_char_equiv' [constructor] (X Y : Type*) :
+  (X ≃* Y) ≃ Σ(f : X →* Y), is_equiv f :=
+begin
+  fapply equiv.MK,
+  { intro e, exact ⟨ pequiv.to_pmap e , pequiv.to_is_equiv e ⟩ },
+  { intro w, exact pequiv_of_pmap w.1 w.2 },
+  { intro w, induction w with f p, fapply sigma_eq,
+    { reflexivity }, { apply is_prop.elimo } },
+  { intro e, apply pequiv_eq, fapply phomotopy.mk,
+    { intro x, reflexivity },
+    { refine !idp_con ⬝ _, reflexivity } }
+end
+
 definition pType_eq_equiv (X Y : Type*) : (X = Y) ≃ (X ≃* Y) :=
 begin
   refine eq_equiv_fn_eq pType.sigma_char' X Y ⬝e !sigma_eq_equiv ⬝e _, esimp,