{A : Type} {B : A -> Type} {C : Type} {x1 x2 : A} (p : x1 = x2) (f : B x1 -> C) {y1 y2 : B x2} (q : y1 = y2) : ap (transport (fun x => B x -> C) p f) q @ transport_arrow_toconst p f y2 = transport_arrow_toconst p f y1 @ ap (fun y => f (p^ # y)) q. Proof. destruct p, q; reflexivity. Defined.
Require Import Basics.Overture Basics.PathGroupoids Basics.Decidable Require Import Types.Forall.