nLab Daniel Licata

Selected writings

Selected writings

On programming in homotopy type theory:

  • Programming in Homotopy Type Theory, Talk at IFIP Wroking Group 2.8 meeting, November, 2012 (pdf, pdf)

Introduction to basics of synthetic homotopy theory in terms of homotopy type theory:

Formalization of (the proof of) the Blakers-Massey theorem in homotopy type theory:

On adjoint logic:

On synthetic (∞,1)-category theory in cubical type theory with bicubical sets:

  • Matthew Weaver, Daniel Licata, A Constructive Model of Directed Univalence in Bicubical Sets, in: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS ’20, Association for Computing Machinery (2020) 915–928 [doi:10.1145/3373718.3394794]

On homotopy dependent linear type theory of dependent stable homotopy types with categorical semantics in parametrized spectra:

category: people

Last revised on October 14, 2023 at 06:27:25. See the history of this page for a list of all contributions to it.