# Dual of the fact that equalizers are dependent sums over the identity type

An equalizer of $$A$$ along two morphisms $$f, g : A \to B$$ can be thought of as a dependent sum over an identity type (see nLab):

$$A|_{f = g} = \sum_{a : A} (f(a) = g(a))$$

Does this idea have a dual? Can we somehow express a coequalizer (quotient type) using dependent products and whatever the "dual of an identity type" is?

• I can't say for sure that the answer is no, I am not an expert in homotopy type theory, but I strongly suspect that to be the case based on my intuition (primarily from coequalizers in $\mathbf{Set}$). The correct type to form coequalizers is the quotient type, which doesn't admit an obvious description in terms of dependent products. Moreover, computing coequalizers is hard in $\mathbf{Set}$, since you have to compute the equivalence relation on $B$ generated by the relations $f(a)\sim g(a)$ for all $a\in A$, which is hard. – jgon May 28 at 6:22