In the presence of $\mathrm{\Sigma }$-types, one may construct all equalizers. Given types $𝐴$ and $𝐵$ with functions $𝑓,𝑔:𝐴\to 𝐵$, the equalizer may be constructed as