proposition: Lemma comm_square_inverse_is_sect {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 wf (comm_square_inverse wf) a @ eissect wB (f a) = ap f (eissect wA a).
proof: Proof. unfold comm_square_inverse, comm_square_comp; simpl. repeat apply (concat (concat_pp_p _ _ _)). apply moveR_Vp. transitivity (ap (wB ^-1 o wB) (ap f (eissect wA a)) @ eissect wB (f a)). 2: apply (concat (concat_Ap (eissect wB) _)). 2: apply ap, ap_idmap. apply (concat (concat_p_pp _ _ _)), whiskerR. apply (concat (ap_pp (wB ^-1) _ _)^), (concatR (ap_compose wB _ _)^). apply ap, (concat (concat_pp_p _ _ _)), moveR_Vp. path_via (ap (f' o wA) (eissect wA a) @ wf a). - apply whiskerR. apply (concatR (ap_compose wA f' _)^). apply ap, eisadj. - apply (concat (concat_Ap wf _)). apply whiskerL, (ap_compose f wB). Defined.
imports: Basics.Overture Basics.PathGroupoids