11 citations · 16 across the 2 of their papers we have counts for
5 papers
Coslice Colimits in Homotopy Type Theory
Perry Hart, Kuen-Bang Hou
We contribute to the theory of (homotopy) colimits inside homotopy type theory. The heart of our work characterizes the connection between (graph-indexed) colimits in a type univer…
The RedPRL Proof Assistant (Invited Paper)
Carlo Angiuli, Evan Cavallo, Kuen-Bang Hou +2
RedPRL is an experimental proof assistant based on Cartesian cubical computational type theory, a new type theory for higher-dimensional constructions inspired by homotopy type the…
Computational Higher Type Theory III: Univalent Universes and Exact Equality
Carlo Angiuli, Kuen-Bang Hou, Robert Harper
This is the third in a series of papers extending Martin-Löf's meaning explanations of dependent type theory to a Cartesian cubical realizability framework that accounts for higher…
A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory
Kuen-Bang Hou, Eric Finster, Dan Licata +1
This paper continues investigations in "synthetic homotopy theory": the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory We present…
A Note on the Uniform Kan Condition in Nominal Cubical Sets
Robert Harper, Kuen-Bang Hou
Bezem, Coquand, and Huber have recently given a constructively valid model of higher type theory in a category of nominal cubical sets satisfying a novel condition, called the unif…