  The study of equality types is central to homotopy type theory.
Characterizing these types is often tricky, and various strategies, such as the
encode-decode method, have been developed.
  We prove a theorem about equality types of coequalizers and pushouts,
reminiscent of an induction principle and without any restrictions on the
truncation levels. This result makes it possible to reason directly about
certain equality types and to streamline existing proofs by eliminating the
necessity of auxiliary constructions.
  To demonstrate this, we give a very short argument for the calculation of the
fundamental group of the circle (Licata and Shulman '13), and for the fact that
pushouts preserve embeddings. Further, our development suggests a higher
version of the Seifert-van Kampen theorem, and the set-truncation operator maps
it to the standard Seifert-van Kampen theorem (due to Favonia and Shulman '16).
  We provide a formalization of the main technical results in the proof
assistant Lean.
