Let quot, canonmap and fac be given.

Assume HE.

Let X and Y be given.

Assume HX HY.

Let f and g be given.

Assume Hf Hg.

An exact proof term for the current goal is equalizer_coequalizer_Op Y X f g (quot Y X f g) (canonmap Y X f g) (fac Y X f g) (HE Y X HY HX f g Hf Hg).

∎