feat(two_quotient): finish proof of elim_incl2

hott/algebra/e_closure.hlean

@@ -33,7 +33,7 @@ section
 
   variables ⦃a a' : A⦄ {s : R a a'} {r : T a a}
   parameter {R}
-  protected definition e_closure.elim [unfold 6] {B : Type} {f : A → B}
+  protected definition e_closure.elim [unfold 8] {B : Type} {f : A → B}
     (e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a') : f a = f a' :=
   begin
     induction t,

hott/hit/torus.hlean

@@ -76,16 +76,13 @@ namespace torus
     (Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1) : ap (torus.elim Pb Pl1 Pl2 Ps) loop2 = Pl2 :=
   !elim_incl1
 
-/-
-  TODO(Leo): uncomment after we finish elim_incl2
   definition elim_surf {P : Type} (Pb : P) (Pl1 : Pb = Pb) (Pl2 : Pb = Pb)
     (Ps : Pl1 ⬝ Pl2 = Pl2 ⬝ Pl1)
-  : square (ap02 (torus.elim Pb Pl1 Pl2 Ps) surf)
+    : square (ap02 (torus.elim Pb Pl1 Pl2 Ps) surf)
-           Ps
+             Ps
-           (!ap_con ⬝ (!elim_loop1 ◾ !elim_loop2))
+             (!ap_con ⬝ (!elim_loop1 ◾ !elim_loop2))
-           (!ap_con ⬝ (!elim_loop2 ◾ !elim_loop1)) :=
+             (!ap_con ⬝ (!elim_loop2 ◾ !elim_loop1)) :=
   !elim_incl2
--/
 
 end torus
 

hott/hit/two_quotient.hlean

@@ -296,21 +296,29 @@ namespace two_quotient
     ⦃a a' : A⦄ (t : T a a') : ap (elim P0 P1 P2) (inclt t) = e_closure.elim P1 t :=
   !elim_inclt --ap_e_closure_elim_h incl1 (elim_incl1 P2) t
 
-/-
-  --print elim
   theorem elim_incl2 {P : Type} (P0 : A → P)
     (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a')
     (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t')
     ⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t')
     : square (ap02 (elim P0 P1 P2) (incl2 q)) (P2 q) (elim_inclt P2 t) (elim_inclt P2 t') :=
   begin
-    -- let H := elim_incl2 R Q2 P0 P1 (two_quotient_Q.rec (λ (a a' : A) (t t' : T a a') (q : Q t t'), con_inv_eq_idp (P2 q))) (Qmk R q),
-    -- esimp at H,
     rewrite [↑[incl2,elim],ap_eq_of_con_inv_eq_idp],
-    xrewrite [eq_top_of_square (elim_incl2 R Q2 P0 P1 (elim_1 A R Q P P0 P1 P2) (Qmk R q)),▸*],
+    xrewrite [eq_top_of_square (elim_incl2 R Q2 P0 P1 (elim_1 A R Q P P0 P1 P2) (Qmk R q))],
-    exact sorry
+--    esimp, --doesn't fold elim_inclt back. The following tactic is just a "custom esimp"
+    xrewrite [{simple_two_quotient.elim_inclt R Q2 (elim_1 A R Q P P0 P1 P2)
+           (t ⬝r t'⁻¹ʳ)}
+      idpath (ap_con (simple_two_quotient.elim R Q2 P0 P1 (elim_1 A R Q P P0 P1 P2))
+                     (inclt t) (inclt t')⁻¹ ⬝
+             (simple_two_quotient.elim_inclt R Q2 (elim_1 A R Q P P0 P1 P2) t ◾
+             (ap_inv (simple_two_quotient.elim R Q2 P0 P1 (elim_1 A R Q P P0 P1 P2))
+                     (inclt t') ⬝
+             inverse2 (simple_two_quotient.elim_inclt R Q2 (elim_1 A R Q P P0 P1 P2) t')))),▸*],
+    rewrite [-con.assoc _ _ (con_inv_eq_idp _),-con.assoc _ _ (_ ◾ _),con.assoc _ _ (ap_con _ _ _),
+             con.left_inv,↑whisker_left,con2_con_con2,-con.assoc (ap_inv _ _)⁻¹,
+             con.left_inv,+idp_con,eq_of_con_inv_eq_idp_con2],
+    xrewrite [to_left_inv !eq_equiv_con_inv_eq_idp (P2 q)],
+    apply top_deg_square
   end
--/
 
 end
 end two_quotient

hott/init/equiv.hlean

@@ -167,14 +167,14 @@ namespace is_equiv
   -- once pulled back along an equivalence f : A → B, then it has a section
   -- over all of B.
 
-  definition equiv_rect (P : B → Type) :
+  definition is_equiv_rect (P : B → Type) :
       (Πx, P (f x)) → (Πy, P y) :=
     (λg y, eq.transport _ (right_inv f y) (g (f⁻¹ y)))
 
-  definition equiv_rect_comp (P : B → Type)
+  definition is_equiv_rect_comp (P : B → Type)
-      (df : Π (x : A), P (f x)) (x : A) : equiv_rect f P df (f x) = df x :=
+      (df : Π (x : A), P (f x)) (x : A) : is_equiv_rect f P df (f x) = df x :=
     calc
-      equiv_rect f P df (f x)
+      is_equiv_rect f P df (f x)
             = right_inv f (f x) ▸ df (f⁻¹ (f x))   : by esimp
         ... = ap f (left_inv f x) ▸ df (f⁻¹ (f x)) : by rewrite -adj
         ... = left_inv f x ▸ df (f⁻¹ (f x))        : by rewrite -transport_compose
@@ -285,6 +285,20 @@ namespace equiv
 
   definition equiv_lift (A : Type) : A ≃ lift A := equiv.mk up _
 
+  definition equiv_rect (f : A ≃ B) (P : B → Type) :
+      (Πx, P (f x)) → (Πy, P y) :=
+    (λg y, eq.transport _ (right_inv f y) (g (f⁻¹ y)))
+
+  definition equiv_rect_comp (f : A ≃ B) (P : B → Type)
+      (df : Π (x : A), P (f x)) (x : A) : equiv_rect f P df (f x) = df x :=
+    calc
+      equiv_rect f P df (f x)
+            = right_inv f (f x) ▸ df (f⁻¹ (f x))   : by esimp
+        ... = ap f (left_inv f x) ▸ df (f⁻¹ (f x)) : by rewrite -adj
+        ... = left_inv f x ▸ df (f⁻¹ (f x))        : by rewrite -transport_compose
+        ... = df x                                 : by rewrite (apd df (left_inv f x))
+
+
   namespace ops
     postfix `⁻¹` := equiv.symm -- overloaded notation for inverse
   end ops

hott/init/path.hlean

@@ -165,10 +165,10 @@ namespace eq
   definition inv_eq_of_idp_eq_con' {p : x = y} {q : y = x} : idp = p ⬝ q → p⁻¹ = q :=
   eq.rec_on p (take q h, h ⬝ !idp_con) q
 
-  definition con_inv_eq_idp {p q : x = y} (r : p = q) : p ⬝ q⁻¹ = idp :=
+  definition con_inv_eq_idp [unfold 6] {p q : x = y} (r : p = q) : p ⬝ q⁻¹ = idp :=
   by cases r;apply con.right_inv
 
-  definition inv_con_eq_idp {p q : x = y} (r : p = q) : q⁻¹ ⬝ p = idp :=
+  definition inv_con_eq_idp [unfold 6] {p q : x = y} (r : p = q) : q⁻¹ ⬝ p = idp :=
   by cases r;apply con.left_inv
 
   definition con_eq_idp {p : x = y} {q : y = x} (r : p = q⁻¹) : p ⬝ q = idp :=
@@ -544,7 +544,7 @@ namespace eq
   /- The 2-dimensional groupoid structure -/
 
   -- Horizontal composition of 2-dimensional paths.
-  definition concat2 {p p' : x = y} {q q' : y = z} (h : p = p') (h' : q = q')
+  definition concat2 [unfold 9 10] {p p' : x = y} {q q' : y = z} (h : p = p') (h' : q = q')
     : p ⬝ q = p' ⬝ q' :=
   eq.rec_on h (eq.rec_on h' idp)
 

hott/init/pathover.hlean

@@ -62,7 +62,7 @@ namespace eq
   by cases p;exact idpo
 
   definition tr_pathover [unfold 5] (p : a = a₂) (b : B a₂) : p⁻¹ ▸ b =[p] b :=
-  pathover_of_eq_tr idp
+  by cases p;exact idpo
 
   definition concato [unfold 12] (r : b =[p] b₂) (r₂ : b₂ =[p₂] b₃) : b =[p ⬝ p₂] b₃ :=
   pathover.rec_on r₂ r
@@ -237,7 +237,7 @@ namespace eq
     : eq_concato q⁻¹ (pathover_idp_of_eq q) = (idpo : b' =[refl a] b') :=
   by induction q;constructor
 
-  definition change_path (q : p = p') (r : b =[p] b₂) : b =[p'] b₂ :=
+  definition change_path [unfold 9] (q : p = p') (r : b =[p] b₂) : b =[p'] b₂ :=
   by induction q;exact r
 
   definition change_path_equiv (f : Π{a}, B a ≃ B' a) (r : b =[p] b₂) : f b =[p] f b₂ :=

hott/types/cubical/cube.hlean

@@ -47,7 +47,7 @@ namespace eq
 
   definition eq_of_cube (c : cube s₁₁₀ s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁) :
     transpose s₁₀₁⁻¹ᵛ ⬝h s₁₁₀ ⬝h transpose s₁₂₁ =
-      whisker_square (eq_bottom_of_square s₀₁₁) (eq_bottom_of_square s₂₁₁) idp idp s₁₁₂ :=
+      whisker_square (eq_bot_of_square s₀₁₁) (eq_bot_of_square s₂₁₁) idp idp s₁₁₂ :=
   by induction c; reflexivity
 
   --set_option pp.implicit true

hott/types/cubical/square.hlean

@@ -134,7 +134,7 @@ namespace eq
   definition square_of_eq_top (r : p₁₀ = p₀₁ ⬝ p₁₂ ⬝ p₂₁⁻¹) : square p₁₀ p₁₂ p₀₁ p₂₁ :=
   by induction p₂₁; induction p₁₂; esimp at r;induction r;induction p₁₀;exact ids
 
-  definition eq_bottom_of_square [unfold 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁)
+  definition eq_bot_of_square [unfold 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁)
     : p₁₂ = p₀₁⁻¹ ⬝ p₁₀ ⬝ p₂₁ :=
   by induction s₁₁; apply idp
 
@@ -165,6 +165,10 @@ namespace eq
     : square (l ⬝ b ⬝ r⁻¹) b l r :=
   by induction r;induction b;induction l;constructor
 
+  definition bot_deg_square (l : a₁ = a₂) (t : a₁ = a₃) (r : a₃ = a₄)
+    : square t (l⁻¹ ⬝ t ⬝ r) l r :=
+  by induction r;induction t;induction l;constructor
+
   /-
     the following two equivalences have as underlying inverse function the functions
     hdeg_square and vdeg_square, respectively.

hott/types/cubical/squareover.hlean

@@ -60,8 +60,8 @@ namespace eq
     : squareover B vrfl q₁₀ q₁₀' idpo idpo :=
   by induction r;exact vrflo
 
-  definition hdeg_squareover {q₁₀' : b₀₀ =[p₁₀] b₂₀} (r : q₁₀ = q₁₀')
+  definition hdeg_squareover {q₀₁' : b₀₀ =[p₀₁] b₀₂} (r : q₀₁ = q₀₁')
-    : squareover B hrfl idpo idpo q₁₀ q₁₀' :=
+    : squareover B hrfl idpo idpo q₀₁ q₀₁' :=
   by induction r; exact hrflo
 
   -- relating squareovers to squares
@@ -120,6 +120,22 @@ namespace eq
     : squareover B (square_of_eq_top s) q₁₀ q₁₂ q₀₁ q₂₁ :=
   by induction q₂₁; induction q₁₂; esimp at r;induction r;induction q₁₀;constructor
 
+  definition squareover_of_eq_top (r : change_path (eq_top_of_square s₁₁) q₁₀ = q₀₁ ⬝o q₁₂ ⬝o q₂₁⁻¹ᵒ)
+    : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁ :=
+  begin
+    induction s₁₁, revert q₁₂ q₁₀ r,
+    eapply idp_rec_on q₂₁, clear q₂₁,
+    intro q₁₂,
+    eapply idp_rec_on q₁₂, clear q₁₂,
+    esimp, intros,
+    induction r, eapply idp_rec_on q₁₀,
+    constructor
+  end
+
+  definition eq_top_of_squareover (r : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁)
+    : change_path (eq_top_of_square s₁₁) q₁₀ = q₀₁ ⬝o q₁₂ ⬝o q₂₁⁻¹ᵒ :=
+  by induction r; reflexivity
+
   /-
   definition squareover_equiv_pathover (q₁₀ : b₀₀ =[p₁₀] b₂₀) (q₁₂ : b₀₂ =[p₁₂] b₂₂)
     (q₀₁ : b₀₀ =[p₀₁] b₀₂) (q₂₁ : b₂₀ =[p₂₁] b₂₂)
@@ -156,6 +172,8 @@ namespace eq
     (s : squareover B (natural_square_tr q p) r r₂
                       (pathover_ap B f (apdo b p)) (pathover_ap B g (apdo b₂ p)))
     : pathover (λa, pathover B (b a) (q a) (b₂ a)) r p r₂ :=
-  by induction p;esimp at s; apply pathover_idp_of_eq; apply eq_of_vdeg_squareover; exact s
+  begin
+    induction p, esimp at s, apply pathover_idp_of_eq, apply eq_of_vdeg_squareover, exact s
+  end
 
 end eq

hott/types/eq.hlean

@@ -252,7 +252,7 @@ namespace eq
   definition eq_equiv_eq_closed [constructor] (p : a₁ = a₂) (q : a₃ = a₄) : (a₁ = a₃) ≃ (a₂ = a₄) :=
   equiv.trans (equiv_eq_closed_left a₃ p) (equiv_eq_closed_right a₂ q)
 
-  definition is_equiv_whisker_left (p : a₁ = a₂) (q r : a₂ = a₃)
+  definition is_equiv_whisker_left [constructor] (p : a₁ = a₂) (q r : a₂ = a₃)
   : is_equiv (whisker_left p : q = r → p ⬝ q = p ⬝ r) :=
   begin
   fapply adjointify,
@@ -269,10 +269,11 @@ namespace eq
     {intro s, induction s, induction q, induction p, reflexivity}
   end
 
-  definition eq_equiv_con_eq_con_left (p : a₁ = a₂) (q r : a₂ = a₃) : (q = r) ≃ (p ⬝ q = p ⬝ r) :=
+  definition eq_equiv_con_eq_con_left [constructor] (p : a₁ = a₂) (q r : a₂ = a₃)
+    : (q = r) ≃ (p ⬝ q = p ⬝ r) :=
   equiv.mk _ !is_equiv_whisker_left
 
-  definition is_equiv_whisker_right {p q : a₁ = a₂} (r : a₂ = a₃)
+  definition is_equiv_whisker_right [constructor] {p q : a₁ = a₂} (r : a₂ = a₃)
     : is_equiv (λs, whisker_right s r : p = q → p ⬝ r = q ⬝ r) :=
   begin
   fapply adjointify,
@@ -281,7 +282,8 @@ namespace eq
     {intro s, induction s, induction r, induction p, reflexivity}
   end
 
-  definition eq_equiv_con_eq_con_right (p q : a₁ = a₂) (r : a₂ = a₃) : (p = q) ≃ (p ⬝ r = q ⬝ r) :=
+  definition eq_equiv_con_eq_con_right [constructor] (p q : a₁ = a₂) (r : a₂ = a₃)
+    : (p = q) ≃ (p ⬝ r = q ⬝ r) :=
   equiv.mk _ !is_equiv_whisker_right
 
   /-
@@ -289,7 +291,7 @@ namespace eq
     However, these proofs have the advantage that the inverse is definitionally equal to
     what we would expect
   -/
-  definition is_equiv_con_eq_of_eq_inv_con (p : a₁ = a₃) (q : a₂ = a₃) (r : a₂ = a₁)
+  definition is_equiv_con_eq_of_eq_inv_con [constructor] (p : a₁ = a₃) (q : a₂ = a₃) (r : a₂ = a₁)
     : is_equiv (con_eq_of_eq_inv_con : p = r⁻¹ ⬝ q → r ⬝ p = q) :=
   begin
     fapply adjointify,
@@ -300,11 +302,11 @@ namespace eq
         con.assoc,con.assoc,con.right_inv,▸*,-con.assoc,con.left_inv,▸* at *,idp_con s] },
   end
 
-  definition eq_inv_con_equiv_con_eq (p : a₁ = a₃) (q : a₂ = a₃) (r : a₂ = a₁)
+  definition eq_inv_con_equiv_con_eq [constructor] (p : a₁ = a₃) (q : a₂ = a₃) (r : a₂ = a₁)
     : (p = r⁻¹ ⬝ q) ≃ (r ⬝ p = q) :=
   equiv.mk _ !is_equiv_con_eq_of_eq_inv_con
 
-  definition is_equiv_con_eq_of_eq_con_inv (p : a₁ = a₃) (q : a₂ = a₃) (r : a₂ = a₁)
+  definition is_equiv_con_eq_of_eq_con_inv [constructor] (p : a₁ = a₃) (q : a₂ = a₃) (r : a₂ = a₁)
     : is_equiv (con_eq_of_eq_con_inv : r = q ⬝ p⁻¹ → r ⬝ p = q) :=
   begin
     fapply adjointify,
@@ -313,11 +315,11 @@ namespace eq
     { intro s, induction p, rewrite [↑[con_eq_of_eq_con_inv,eq_con_inv_of_con_eq]] },
   end
 
-  definition eq_con_inv_equiv_con_eq (p : a₁ = a₃) (q : a₂ = a₃) (r : a₂ = a₁)
+  definition eq_con_inv_equiv_con_eq [constructor] (p : a₁ = a₃) (q : a₂ = a₃) (r : a₂ = a₁)
     : (r = q ⬝ p⁻¹) ≃ (r ⬝ p = q) :=
   equiv.mk _ !is_equiv_con_eq_of_eq_con_inv
 
-  definition is_equiv_inv_con_eq_of_eq_con (p : a₁ = a₃) (q : a₂ = a₃) (r : a₁ = a₂)
+  definition is_equiv_inv_con_eq_of_eq_con [constructor] (p : a₁ = a₃) (q : a₂ = a₃) (r : a₁ = a₂)
     : is_equiv (inv_con_eq_of_eq_con : p = r ⬝ q → r⁻¹ ⬝ p = q) :=
   begin
     fapply adjointify,
@@ -328,11 +330,11 @@ namespace eq
         con.assoc,con.assoc,con.right_inv,▸*,-con.assoc,con.left_inv,▸* at *,idp_con s] },
   end
 
-  definition eq_con_equiv_inv_con_eq (p : a₁ = a₃) (q : a₂ = a₃) (r : a₁ = a₂)
+  definition eq_con_equiv_inv_con_eq [constructor] (p : a₁ = a₃) (q : a₂ = a₃) (r : a₁ = a₂)
     : (p = r ⬝ q) ≃ (r⁻¹ ⬝ p = q) :=
   equiv.mk _ !is_equiv_inv_con_eq_of_eq_con
 
-  definition is_equiv_con_inv_eq_of_eq_con (p : a₃ = a₁) (q : a₂ = a₃) (r : a₂ = a₁)
+  definition is_equiv_con_inv_eq_of_eq_con [constructor] (p : a₃ = a₁) (q : a₂ = a₃) (r : a₂ = a₁)
     : is_equiv (con_inv_eq_of_eq_con : r = q ⬝ p → r ⬝ p⁻¹ = q) :=
   begin
     fapply adjointify,
@@ -366,6 +368,32 @@ namespace eq
     : is_equiv (eq_inv_con_of_con_eq : r ⬝ p = q → p = r⁻¹ ⬝ q) :=
   is_equiv_inv con_eq_of_eq_inv_con
 
+  definition is_equiv_con_inv_eq_idp [constructor] (p q : a₁ = a₂)
+    : is_equiv (con_inv_eq_idp : p = q → p ⬝ q⁻¹ = idp) :=
+  begin
+    fapply adjointify,
+    { apply eq_of_con_inv_eq_idp},
+    { intro s, induction q, esimp at *, cases s, reflexivity},
+    { intro s, induction s, induction p, reflexivity},
+  end
+
+  definition is_equiv_inv_con_eq_idp [constructor] (p q : a₁ = a₂)
+    : is_equiv (inv_con_eq_idp : p = q → q⁻¹ ⬝ p = idp) :=
+  begin
+    fapply adjointify,
+    { apply eq_of_inv_con_eq_idp},
+    { intro s, induction q, esimp [eq_of_inv_con_eq_idp] at *,
+      eapply is_equiv_rect (eq_equiv_con_eq_con_left idp p idp), clear s,
+      intro s, cases s, reflexivity},
+    { intro s, induction s, induction p, reflexivity},
+  end
+
+  definition eq_equiv_con_inv_eq_idp [constructor] (p q : a₁ = a₂) : (p = q) ≃ (p ⬝ q⁻¹ = idp) :=
+  equiv.mk _ !is_equiv_con_inv_eq_idp
+
+  definition eq_equiv_inv_con_eq_idp [constructor] (p q : a₁ = a₂) : (p = q) ≃ (q⁻¹ ⬝ p = idp) :=
+  equiv.mk _ !is_equiv_inv_con_eq_idp
+
   /- Pathover Equivalences -/
 
   definition pathover_eq_equiv_l (p : a₁ = a₂) (q : a₁ = a₃) (r : a₂ = a₃) : q =[p] r ≃ q = p ⬝ r :=

hott/types/eq2.hlean

@@ -96,6 +96,11 @@ namespace eq
             :=
   by induction q;esimp at *;cases r;reflexivity
 
+  theorem eq_of_con_inv_eq_idp_con2 {p p' q q' : a₁ = a₂} (r : p = p') (s : q = q')
+    (t : p' ⬝ q'⁻¹ = idp)
+  : eq_of_con_inv_eq_idp (r ◾ inverse2 s ⬝ t) = r ⬝ eq_of_con_inv_eq_idp t ⬝ s⁻¹ :=
+  by induction s;induction r;induction q;reflexivity
+
 -- definition naturality_apdo {A : Type} {B : A → Type} {a a₂ : A} {f g : Πa, B a}
 --   (H : f ~ g) (p : a = a₂)
 --   : squareover B vrfl (apdo f p) (apdo g p)

hott/types/pi.hlean

@@ -159,7 +159,7 @@ namespace pi
     : ap (pi_functor f0 f1) (eq_of_homotopy h)
       = eq_of_homotopy (λa':A', (ap (f1 a') (h (f0 a')))) :=
   begin
-  apply (equiv_rect (@apd10 A B g g')), intro p, clear h,
+  apply (is_equiv_rect (@apd10 A B g g')), intro p, clear h,
   cases p,
   apply concat,
     exact (ap (ap (pi_functor f0 f1)) (eq_of_homotopy_idp g)),