Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory
(2020)
Presentation / Conference Contribution
Kraus, N., & Von Raumer, J. (2020). Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory. In LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (662-675). https://doi.org/10.1145/3373718.3394800
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.