proposition: Lemma comm_square_inverse_is_retr {A B : Type} {f : A -> B} {A' B' : Type} {f' : A' -> B'} (wA : A <~> A') (wB : B <~> B') (wf : f' o wA == wB o f) (a : A') : comm_square_comp (comm_square_inverse wf) wf a @ eisretr wB (f' a) = ap f' (eisretr wA a).
proof: Proof. unfold comm_square_inverse, comm_square_comp; simpl. rewrite !ap_pp. rewrite <- !concat_pp_p. rewrite concat_pp_p. set (p := (ap wB (ap (wB ^-1) (ap f' (eisretr wA a))) @ eisretr wB (f' a))). path_via ((eisretr wB _)^ @ p). - apply whiskerR. apply moveR_pM. path_via ((eisretr wB (f' (wA (wA ^-1 a))))^ @ ap (wB o wB ^-1) (wf ((wA ^-1) a))). + rewrite ap_V, <- eisadj. transitivity (ap idmap (wf ((wA ^-1) a)) @ (eisretr wB (wB (f ((wA ^-1) a))))^). * apply whiskerR, inverse, ap_idmap. * apply (concat_Ap (fun b' => (eisretr wB b')^) _). + apply ap. rewrite ap_compose, !ap_V. apply inverse, inv_V. - apply moveR_Vp. subst p. rewrite <- ap_compose. path_via (eisretr wB _ @ ap idmap (ap f' (eisretr wA a))). + apply (concat_Ap (eisretr wB) _). + apply ap, ap_idmap. Defined.
imports: Basics.Overture Basics.PathGroupoids