From 33e948d9d1b3e2b62993690fe4f06aedda62d104 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 4 Jun 2015 01:09:26 -0400
Subject: [PATCH] feat(hit/sphere): Prove that maps from S^n to an (n-1)-type
 are constant

---
 hott/hit/sphere.hlean    | 41 +++++++++++++++++++++++++++++++++++-----
 hott/types/pointed.hlean | 20 ++++++++++++++++----
 hott/types/trunc.hlean   |  2 +-
 3 files changed, 53 insertions(+), 10 deletions(-)

diff --git a/hott/hit/sphere.hlean b/hott/hit/sphere.hlean
index 879088f0e..2abb6e247 100644
--- a/hott/hit/sphere.hlean
+++ b/hott/hit/sphere.hlean
@@ -88,11 +88,18 @@ namespace sphere
   definition Sphere [constructor] (n : ℕ) : Pointed := pointed.mk' (sphere n)
 
   namespace ops
-  abbreviation S := sphere
-  notation `S.` := Sphere
+    abbreviation S := sphere
+    notation `S.`:max := Sphere
   end ops
   open sphere.ops
 
+  definition equator (n : ℕ) : map₊ (S. n) (Ω (S. (succ n))) :=
+  pointed_map.mk (λa, merid a ⬝ (merid base)⁻¹) !con.right_inv
+
+  definition surf {n : ℕ} : Ω[n] S. n :=
+  nat.rec_on n (by esimp [Iterated_loop_space]; exact base)
+               (by intro n s;exact apn (equator n) s)
+
   definition bool_of_sphere [reducible] : S 0 → bool :=
   suspension.rec ff tt (λx, empty.elim x)
 
@@ -119,6 +126,16 @@ namespace sphere
     { intro A, transitivity _, apply suspension_adjoint_loop (S. n) A, apply IH}
   end
 
+  protected definition elim {n : ℕ} {P : Pointed} (p : Ω[n] P) : map₊ (S. n) P :=
+  to_inv !pointed_map_sphere p
+
+  definition elim_surf {n : ℕ} {P : Pointed} (p : Ω[n] P) : apn (sphere.elim p) surf = p :=
+  begin
+    induction n with n IH,
+    { esimp [apn,surf,sphere.elim,pointed_map_sphere], apply sorry},
+    { apply sorry}
+  end
+
 end sphere
 
 open sphere sphere.ops
@@ -128,7 +145,8 @@ structure weakly_constant [class] {A B : Type} (f : A → B) := --move
 
 namespace trunc
   open trunc_index
-  definition is_trunc_of_pointed_map_sphere_constant (n : ℕ) (A : Type)
+  variables {n : ℕ} {A : Type}
+  definition is_trunc_of_pointed_map_sphere_constant
     (H : Π(a : A) (f : map₊ (S. n) (pointed.Mk a)) (x : S n), f x = f base) : is_trunc (n.-2.+1) A :=
   begin
     apply iff.elim_right !is_trunc_iff_is_contr_loop,
@@ -141,12 +159,25 @@ namespace trunc
       { rewrite [▸*,con.right_inv,▸*,con.left_inv]}}
   end
 
-
-  definition is_trunc_iff_map_sphere_constant (n : ℕ) (A : Type)
+  definition is_trunc_iff_map_sphere_constant
     (H : Π(f : S n → A) (x : S n), f x = f base) : is_trunc (n.-2.+1) A :=
   begin
     apply is_trunc_of_pointed_map_sphere_constant,
     intros, cases f with f p, esimp at *, apply H
   end
 
+  definition pointed_map_sphere_constant_of_is_trunc [H : is_trunc (n.-2.+1) A]
+    (a : A) (f : map₊ (S. n) (pointed.Mk a)) (x : S n) : f x = f base :=
+  begin
+    let H' := iff.elim_left (is_trunc_iff_is_contr_loop n A) H a,
+    let H'' := @is_trunc_equiv_closed_rev _ _ _ !pointed_map_sphere H',
+    assert p : (f = pointed_map.mk (λx, f base) (respect_pt f)),
+      apply is_hprop.elim,
+    exact ap10 (ap pointed_map.map p) x
+  end
+
+  definition map_sphere_constant_of_is_trunc [H : is_trunc (n.-2.+1) A]
+    (f : S n → A) (x : S n) : f x = f base :=
+  pointed_map_sphere_constant_of_is_trunc (f base) (pointed_map.mk f idp) x
+
 end trunc
diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean
index 727265cce..3e22dedfb 100644
--- a/hott/types/pointed.hlean
+++ b/hott/types/pointed.hlean
@@ -66,11 +66,11 @@ namespace pointed
   -- | Iterated_loop_space A 0 := A
   -- | Iterated_loop_space A (n+1) := Iterated_loop_space (Loop_space A) n
 
-  definition Iterated_loop_space (A : Pointed) (n : ℕ) : Pointed :=
+  definition Iterated_loop_space [reducible] (n : ℕ) (A : Pointed) : Pointed :=
   nat.rec_on n (λA, A) (λn IH A, IH (Loop_space A)) A
 
-  prefix `Ω`:(max+1) := Loop_space
-  notation `Ω[`:95 n:0 `]`:0 A:95 := Iterated_loop_space A n
+  prefix `Ω`:(max+5) := Loop_space
+  notation `Ω[`:95 n:0 `]`:0 A:95 := Iterated_loop_space n A
 
   definition iterated_loop_space (A : Type) [H : pointed A] (n : ℕ) : Type :=
   Ω[n] (pointed.mk' A)
@@ -148,7 +148,6 @@ namespace pointed
   --     }
   -- end
 
-
   definition pointed_map_bool_equiv (B : Pointed) : map₊ Bool B ≃ B :=
   begin
     fapply equiv.MK,
@@ -166,4 +165,17 @@ namespace pointed
   --     ... ≃ (unit → B) : pointed_map_equiv
   --     ... ≃ B : unit_imp_equiv
 
+  definition apn {A B : Pointed} {n : ℕ} (f : map₊ A B) (p : Ω[n] A) : Ω[n] B :=
+  begin
+  revert A B f p, induction n with n IH,
+  { intros A B f p, exact f p},
+  { intros A B f p, rewrite [↑Iterated_loop_space at p,↓Iterated_loop_space n (Ω A) at p,
+      ↑Iterated_loop_space, ↓Iterated_loop_space n (Ω B)],
+    apply IH (Ω A),
+    { esimp, fapply pointed_map.mk,
+        intro q, refine !respect_pt⁻¹ ⬝ ap f q ⬝ !respect_pt,
+        esimp, apply con.left_inv},
+    { exact p}}
+  end
+
 end pointed
diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean
index 3d6a6d7f2..b44370e60 100644
--- a/hott/types/trunc.hlean
+++ b/hott/types/trunc.hlean
@@ -171,7 +171,7 @@ namespace is_trunc
           { esimp, apply con_right_inv2}},
         transitivity _,
           apply iff.pi_iff_pi, intro p,
-          rewrite [↑Iterated_loop_space,↓Iterated_loop_space (Loop_space (pointed.Mk p)) n,H],
+          rewrite [↑Iterated_loop_space,↓Iterated_loop_space n (Loop_space (pointed.Mk p)),H],
           apply iff.refl,
         apply iff.imp_iff, reflexivity}
   end