nLab Favonia

Known also as Kuen-Bang Hou (Favonia).

• page on HoTT website

• homepage

• Higher-Dimensional Types in the Mechanization of Homotopy Theory, PhD thesis 2017, (webpage, pdf direct link)

Selected writings

On (homotopy types of) covering spaces via homotopy type theory:

• Kuen-Bang Hou, Covering Spaces in Homotopy Type Theory, extended abstract Type Theory, Homotopy Theory and Univalent Foundations (2013) $[$doi:10.1007/978-3-319-21284-5_15$]$

• Kuen-Bang Hou, Robert Harper, Covering Spaces in Homotopy Type Theory, Leibniz International Proceedings in Informatics (LIPIcs) 97 (2018) $[$doi:10.4230/LIPIcs.TYPES.2016.11, pdf$]$

Formalization of (the proof of) the Blakers-Massey theorem in homotopy type theory:

• Kuen-Bang Hou (Favonia), Eric Finster, Dan Licata, Peter LeFanu Lumsdaine, A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory, LICS ‘16 (2016) 565–574 [arXiv.1605.03227, doi:10.1145/2933575.2934545]

On cellular cohomology formulated in homotopy type theory:

• Ulrik Buchholtz, Kuen-Bang Hou (Favonia), Cellular Cohomology in Homotopy Type Theory, Logical Methods in Computer Science, Volume 16, Issue 2 (June 1, 2020) (arXiv:1802.02191, lmcs:6518)

On universe polymorphism in dependent type theory via monads:

• Favonia, Carlo Angiuli, Reed Mullanix, An Order-Theoretic Analysis of Universe Polymorphism, Proceedings of the ACM on Programming Languages 7 57 (2023) 1659–1685 [doi:10.1145/3571250]

Related entries

• homotopy type theory

• Blakers-Massey theorem

category: people