Timings for Equalizer.v
Require Import Basics Types.Sigma Types.Paths.
Definition Equalizer {A B} (f g : A -> B)
:= {x : A & f x = g x}.
Definition functor_equalizer {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'.
exact ((p x)^ @ (ap h r) @ (q x)).
Definition equiv_functor_equalizer {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'.
srapply (equiv_functor_sigma' k).
exact (equiv_concat_r (q a) _ oE equiv_concat_l (p a)^ _).