34 citations · 95 across the 15 of their papers we have counts for
5 papers · 1 filter
Central H-spaces and banded types
Ulrik Buchholtz, J. Daniel Christensen, Jarl G. Taxerås Flaten +1
We introduce and study central types, which are generalizations of Eilenberg-Mac Lane spaces. A type is central when it is equivalent to the component of the identity among its own…
The long exact sequence of homotopy -groups
Ulrik Buchholtz, Egbert Rijke
Working in homotopy type theory, we introduce the notion of -exactness for a short sequence of pointed types, and show that any fiber sequence $F\hookrightarrow E…
Localization in Homotopy Type Theory
J. Daniel Christensen, Morgan Opie, Egbert Rijke +1
We study localization at a prime in homotopy type theory, using self maps of the circle. Our main result is that for a pointed, simply connected type , the natural map $X \to X_…
The real projective spaces in homotopy type theory
Ulrik Buchholtz, Egbert Rijke
Homotopy type theory is a version of Martin-Löf type theory taking advantage of its homotopical models. In particular, we can use and construct objects of homotopy theory and reaso…
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…