{A B A' B'} (f g : A -> B) (f' g' : A' -> B') (h : B -> B') (k : A -> A') (p : h o f == f' o k) (q : h o g == g' o k) : Equalizer f g -> Equalizer f' g'. Proof. intros [x r]. exists (k x). exact ((p x)^ @ (ap h r) @ (q x)). Defined.
Require Import Basics Types.Sigma Types.Paths.