minor additions

heq.hlean

@@ -2,7 +2,7 @@
 
 open eq is_trunc
 
-variables {I : Set} {P : I → Type} {i j k : I} {x x₁ x₂ : P i} {y y₁ y₂ : P j} {z : P k}
+variables {I : Type} [is_set I] {P : I → Type} {i j k : I} {x x₁ x₂ : P i} {y y₁ y₂ : P j} {z : P k}
           {Q : Π⦃i⦄, P i → Type}
 
 structure heq (x : P i) (y : P j) : Type :=
@@ -10,7 +10,7 @@ structure heq (x : P i) (y : P j) : Type :=
   (q : x =[p] y)
 
 namespace eq
-notation x ` ==[`:50 P:0 `] `:0 y:50 := @heq _ P _ _ x y
+notation x ` ==[`:50 P:0 `] `:0 y:50 := @heq _ _ P _ _ x y
 infix ` == `:50 := heq -- mostly for printing, since it will be almost always ambiguous what P is
 
 definition pathover_of_heq {p : i = j} (q : x ==[P] y) : x =[p] y :=

homotopy/EM.hlean

@@ -7,8 +7,31 @@ open eq equiv is_equiv algebra group nat pointed EM.ops is_trunc trunc susp func
 universe variable u
 /- TODO: try to fix the compilation time of this file -/
 
+
 namespace EM
 
+  /- move to HoTT-EM, this version doesn't require that X is connected -/
+  definition EM1_map' [unfold 6] {G : Group} {X : Type*} (e : G → Ω X)
+    (r : Πg h, e (g * h) = e g ⬝ e h) [is_trunc 1 X] : EM1 G → X :=
+  begin
+    intro x, induction x using EM.elim,
+    { exact Point X },
+    { exact e g },
+    { exact r g h }
+  end
+
+  definition EM1_pmap' [constructor] {G : Group} {X : Type*} (e : G → Ω X)
+    (r : Πg h, e (g * h) = e g ⬝ e h) [is_trunc 1 X] : EM1 G →* X :=
+  pmap.mk (EM1_map' e r) idp
+
+  definition loop_EM1_pmap' {G : Group} {X : Type*} (e : G →* Ω X)
+    (r : Πg h, e (g * h) = e g ⬝ e h) [is_trunc 1 X] : Ω→(EM1_pmap' e r) ∘* loop_EM1 G ~* e :=
+  begin
+    fapply phomotopy.mk,
+    { intro g, refine !idp_con ⬝ elim_pth r g },
+    { apply is_set.elim }
+  end
+
   definition EMadd1_functor_succ [unfold_full] {G H : AbGroup} (φ : G →g H) (n : ℕ) :
     EMadd1_functor φ (succ n) ~* ptrunc_functor (n+2) (susp_functor (EMadd1_functor φ n)) :=
   by reflexivity

move_to_lib.hlean

@@ -890,6 +890,12 @@ end is_trunc
 namespace sigma
   open sigma.ops
 
+definition sigma_functor2 [constructor] {A₁ A₂ A₃ : Type}
+  {B₁ : A₁ → Type} {B₂ : A₂ → Type} {B₃ : A₃ → Type}
+  (f : A₁ → A₂ → A₃) (g : Π⦃a₁ a₂⦄, B₁ a₁ → B₂ a₂ → B₃ (f a₁ a₂))
+    (x₁ : Σa₁, B₁ a₁) (x₂ : Σa₂, B₂ a₂) : Σa₃, B₃ a₃ :=
+⟨f x₁.1 x₂.1, g x₁.2 x₂.2⟩
+
 definition eq.rec_sigma {A : Type} {B : A → Type} {a : A} {b : B a}
   (P : Π⦃a'⦄ {b' : B a'}, ⟨a, b⟩ = ⟨a', b'⟩ → Type)
   (IH : P idp) ⦃a' : A⦄ {b' : B a'} (p : ⟨a, b⟩ = ⟨a', b'⟩) : P p :=
@@ -1301,6 +1307,16 @@ definition is_conn_fiber (n : ℕ₋₂) {A B : Type} (f : A → B) (b : B) [is_
   [is_conn (n.+1) B] : is_conn n (fiber f b) :=
 is_conn_equiv_closed_rev _ !fiber.sigma_char _
 
+definition is_conn_succ_of_is_conn_loop {n : ℕ₋₂} {A : Type*}
+  (H : is_conn 0 A) (H2 : is_conn n (Ω A)) : is_conn (n.+1) A :=
+begin
+  apply is_conn_succ_intro, exact tr pt,
+  intros a a',
+  induction merely_of_minus_one_conn (is_conn_eq -1 a a') with p, induction p,
+  induction merely_of_minus_one_conn (is_conn_eq -1 pt a) with p, induction p,
+  exact H2
+end
+
 definition is_conn_fun_compose {n : ℕ₋₂} {A B C : Type} (g : B → C) (f : A → B)
   (H : is_conn_fun n g) (K : is_conn_fun n f) : is_conn_fun n (g ∘ f) :=
 sorry