Showing math.LOShow all
2 papers · 1 filter
math.LO2020
Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory
Nicolai Kraus, Jakob von Raumer
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 nec…
math.LO2019
Path Spaces of Higher Inductive Types in Homotopy Type Theory
Nicolai Kraus, Jakob von Raumer
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 deve…