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?

  • $\begingroup$ 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. $\endgroup$ – jgon May 28 at 6:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.