proposition: Lemma comm_square_inverse {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) : f o (wA ^-1) == (wB ^-1) o f'.
proof: Proof. intros a'. path_via (wB ^-1 (wB (f (wA ^-1 a')))). - apply inverse, eissect. - apply ap, (concat (wf _)^). apply ap, eisretr. Defined.
imports: Basics.Overture Basics.PathGroupoids