working on the join theorem

homotopy/join_theorem.hlean

@@ -0,0 +1,83 @@
+/-- Authors: Clive, Egbert --/
+
+import homotopy.connectedness homotopy.join
+
+open eq sigma pi function join homotopy is_trunc equiv is_equiv
+
+namespace retraction
+  variables {A B C : Type} (r2 : B → C) (r1 : A → B)
+
+
+  definition is_retraction_compose
+    [Hr2 : is_retraction r2] [Hr1 : is_retraction r1] :
+    is_retraction (r2 ∘ r1) :=
+  begin
+    cases Hr2 with s2 s2_is_right_inverse,
+    cases Hr1 with s1 s1_is_right_inverse,
+    fapply is_retraction.mk,
+    { exact s1 ∘ s2},
+    { intro b, esimp,
+      calc
+      r2 (r1 (s1 (s2 (b)))) = r2 (s2 (b)) : ap r2 (s1_is_right_inverse (s2 b))
+                        ... = b           : s2_is_right_inverse b
+
+    }, /-- QED --/
+  end
+
+  definition is_retraction_compose_equiv_left [Hr2 : is_equiv r2] [Hr1 : is_retraction r1] : is_retraction (r2 ∘ r1) :=
+  begin
+    apply is_retraction_compose,
+  end
+
+  definition is_retraction_compose_equiv_right [Hr2 : is_retraction r2] [Hr1 :  is_equiv r1] : is_retraction (r2 ∘ r1) :=
+  begin
+    apply is_retraction_compose,
+  end
+
+end retraction
+
+namespace is_conn
+section
+
+    open retraction
+
+    universe variable u
+    parameters (n : ℕ₋₂) {A : Type.{u}}
+    parameter sec : ΠV : trunctype.{u} n,
+                    is_retraction (const A : V → (A → V))
+
+    include sec
+
+    protected definition intro : is_conn n A :=
+    begin
+      apply is_conn_of_map_to_unit,
+      apply is_conn_fun.intro,
+      intro P,
+      refine is_retraction_compose_equiv_right (const A) (pi_unit_left P),
+    end
+end
+end is_conn
+
+section Join_Theorem
+
+variables (X Y : Type)
+          (m n : ℕ₋₂)
+          [HXm : is_conn m X]
+          [HYn : is_conn n Y]
+
+include HXm HYn
+
+theorem is_conn_join : is_conn (m +2+ n) (join X Y) :=
+begin
+  apply is_conn.intro,
+  intro V,
+  apply is_retraction_of_is_equiv,
+  apply is_equiv_of_is_contr_fun,
+  intro f,
+  refine is_contr_equiv_closed _,
+  {exact unit},
+  symmetry,
+  exact sorry
+end
+
+end Join_Theorem