Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory
(2020)
Presentation / Conference Contribution
Kraus, N., & Von Raumer, J. (2020, June). Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory. Presented at ACM International Conference Proceeding Series, Saarbrücken Germany (held online)
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.