Authors

- Alexis Hazell? co- or authored: Agda, Categorical Homotopy Type Theory, Formalized Homotopy Theory, Home Page, Homotopy Type System, Martin-Löf Type Theory, Per Martin-Löf, Resources, Uniqueness of Identity Proofs, about, definitional equality, dependent type, higher inductive type, homotopy groups of spheres, inductive-inductive type, inductive-recursive type, loop space, loop space of a wedge of circles, model invariance problem, model of type theory in an (infinity,1)-topos, open problems, semantics, semi-simplicial types, type, type theories, type theory, univalence axiom, universe
- Anonymous Coward? co- or authored: Formalized Homotopy Theory, Home Page, References, open problems, semantics, semi-simplicial types
- Bas Spitters? co- or authored: DMV2015, Home Page, Homotopy Type System, References, algebraic formulation of dependent type theory, elementary (infinity,1)-topos, model of type theory in an (infinity,1)-topos, open problems, proof theoretic strength of univalent type theory plus HITs, realizability, topos, universe
- Bas Spitters co- or authored: Bas Spitters, Formalized Homotopy Theory, Home Page, Homotopy Type System, inductive-inductive type, open problems
- David Roberts co- or authored: David Roberts, Formalized Homotopy Theory, References, homotopy groups of spheres, open problems
- Floris van Doorn? co- or authored: Home Page, References, spectral sequences
- Mike Shulman co- or authored: Agda, Formalized Homotopy Theory, Home Page, Homotopy Type System, Mike Shulman, References, Uniqueness of Identity Proofs, about, axioms, circle, de Morgan's law, definitional equality, higher inductive type, homotopy groups of spheres, limited principle of omniscience, loop space of a wedge of circles, model invariance problem, model of type theory in an (infinity,1)-topos, natural model, open problems, semantics, semi-simplicial types, spectral sequences, the Ho TT book, type theories, univalence axiom, universe
- Steve Awodey? co- or authored: CMU local activities, Categorical Homotopy Type Theory, DMV2015, Ho TT Mini-Course, Home Page, Resources, open problems, semantics, the Ho TT book, type theories
- Steve Awodey? co- or authored: Home Page, References, about, open problems, univalence axiom
- Urs Schreiber co- or authored: Cesare Gallozzi, DMV2015, Denis-Charles Cisinski, Grothendieck (infinity,1)-topos, References, Urs Schreiber, model of type theory in an (infinity,1)-topos, open problems, universe