Homotopy Type Theory

Discussion of Homotopy Type Theory and Univalent Foundations

Showing 1-20 of 603 topics
univalence without coherent equivalences Michael Shulman 8/14/17
[HoTT] Native coinductive records for cubical type theory Andrea Vezzosi 8/11/17
LFMTP '17 in Oxford this September Kristina Sojakova 8/10/17
HoTT/UF 2017: 2nd Call for Participation Benedikt Ahrens 8/10/17
Preprint available: On equality of objects in categories in constructive type theory palmgren 8/5/17
cubical type theory with UIP Michael Shulman 8/2/17
Call for Participation: Workshop on HoTT/UF (with FSCD 2017) Simon 7/28/17
Weaker forms of univalence Ian Orton 7/21/17
Non-enumerability of R Andrej Bauer 7/18/17
Univalent Higher Categories via Complete Semi-Segal Types Nicolai Kraus 7/15/17
trivial cofibration-fibration factorization coquand 7/6/17
differential geometry in modal HoTT Urs Schreiber 6/28/17
Modalities in homotopy type theory Bas Spitters 6/28/17
2nd Call for Contributions and Participation: Workshop on HoTT/UF (with FSCD 2017) Anders Mörtberg 6/20/17
Is "classical" Hedberg's Theorem true? Andrew Polonsky 6/20/17
PSSL 101, September 16th-17th, Leeds (UK) Nicola Gambino 6/19/17
Semantics of higher inductive types Michael Shulman 6/7/17
Logic Colloquium 2017: Call for Registration and Participation ** Deadline for early registration: June 9, 2017 ** palmgren 6/1/17
Does MLTT have "or"? Martín Hötzel Escardó 5/15/17
cubical stacks coquand 5/14/17
More topics »