feat(types/eq2): add theorem about eq_of_con_inv_eq_idp

hott/init/path.hlean

@@ -631,7 +631,8 @@ namespace eq
     ⬝ (!whisker_left_idp_left ◾ !whisker_right_idp_right)
 
   -- The action of functions on 2-dimensional paths
-  definition ap02 [unfold-c 8] (f : A → B) {x y : A} {p q : x = y} (r : p = q) : ap f p = ap f q :=
+  definition ap02 [unfold-c 8] [reducible] (f : A → B) {x y : A} {p q : x = y} (r : p = q)
+    : ap f p = ap f q :=
   ap (ap f) r
 
   definition ap02_con (f : A → B) {x y : A} {p p' p'' : x = y} (r : p = p') (r' : p' = p'') :

hott/types/cubical/square.hlean

@@ -359,4 +359,10 @@ namespace eq
       : square (t₁ ◾ t₂) (b₁ ◾ b₂) (l₁ ◾ l₂) (r₁ ◾ r₂) :=
   by induction s₂;induction s₁;constructor
 
+  -- definition square_of_con_inv_hsquare {p₁ p₂ p₃ p₄ : a₁ = a₂}
+  --   {t : p₁ = p₂} {b : p₃ = p₄} {l : p₁ = p₃} {r : p₂ = p₄}
+  --   (s : square (con_inv_eq_idp t) (con_inv_eq_idp b) (l ◾ r⁻²) idp)
+  --     : square t b l r :=
+  -- sorry --by induction s
+
 end eq

hott/types/eq2.hlean

@@ -90,6 +90,12 @@ namespace eq
            (ap_compose g f q) :=
   natural_square (ap_compose g f) r
 
+  theorem ap_eq_of_con_inv_eq_idp (f : A → B) {p q : a₁ = a₂} (r : p ⬝ q⁻¹ = idp)
+  : ap02 f (eq_of_con_inv_eq_idp r) =
+           eq_of_con_inv_eq_idp (whisker_left _ !ap_inv⁻¹ ⬝ !ap_con⁻¹ ⬝ ap02 f r)
+            :=
+  by induction q;esimp at *;cases r;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)