1 citations · 1 across the 3 of their papers we have counts for
3 papers
math.LO2024
Primitive Recursive Dependent Type Theory
Ulrik Buchholtz, Johannes Schipp von Branitz
We show that restricting the elimination principle of the natural numbers type in Martin-Löf Type Theory (MLTT) to a universe of types not containing -types ensures that all def…
cs.LO2024
On symmetries of spheres in univalent foundations
Pierre Cagne, Ulrik Buchholtz, Nicolai Kraus +1
Working in univalent foundations, we investigate the symmetries of spheres, i.e., the types of the form . The case of the circle has a slick answer: th…
math.AT2016★ 1 cited
The Cayley-Dickson Construction in Homotopy Type Theory
Ulrik Buchholtz, Egbert Rijke
We define in the setting of homotopy type theory an H-space structure on . Hence we obtain a description of the quaternionic Hopf fibration $\mathbb S^3\hookrightarrow…