{A B C} (f : A -> B) (g g' : B -> C) (p : g = g') : transport (fun h : B -> C => g o f = h o f) p 1 = ap (fun h => h o f) p. Proof. destruct p; reflexivity. Defined.
Require Import Basics.Overture Basics.Tactics.