Questions pertaining to equality in type theory (all kinds of equality are included: judgemental, propositional, observational, setoid equality, etc.) and equality reasoning in proof assistants.

References:
nLab