Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory
(2020)
Conference Proceeding
Suppose we are given a graph and want to show a property for all its cycles (closed chains). Induction on the length of cycles does not work since sub-chains of a cycle are not necessarily closed. This paper derives a principle reminiscent of inducti... Read More about Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory.