nLab Daniel Licata

Daniel R. Licata

• personal page

• personal page (old)

• MathGenealogy page

• GoogleScholar page

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:

• Guillaume Brunerie, Dan Licata, Peter LeFanu Lumsdaine: Homotopy theory in type theory, 2013 (pdf slides, pdf, blog entry 1, blog entry 2)

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

• Kuen-Bang Hou (Favonia), Eric Finster, Dan Licata, Peter LeFanu Lumsdaine, A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory, LICS ‘16 (2016) 565–574 [arXiv.1605.03227, doi:10.1145/2933575.2934545]

On adjoint logic:

• Daniel Licata, Mike Shulman, and Mitchell Riley, A Fibrational Framework for Substructural and Modal Logics (extended version), in Proceedings of 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) (doi: 10.4230/LIPIcs.FSCD.2017.25, pdf)

On synthetic mathematics in modal homotopy type theory:

• Dan Licata, Felix Wellen: Synthetic Mathematics in Modal Dependent Type Theories, tutorial at Types, Homotopy Theory and Verification (2018)

  Tutorial 1, Dan Licata: A Fibrational Framework for Modal Simple Type Theories (recording)

  Tutorial 2, Felix Wellen: The Shape Modality in Real cohesive HoTT and Covering Spaces (recording)

  Tutorial 3, Dan Licata: Discrete and Codiscrete Modalities in Cohesive HoTT (recording)

  Tutorial 4, Felix Wellen, Discrete and Codiscrete Modalities in Cohesive HoTT, II (recording)

  Tutorial 5, Dan Licata: A Fibrational Framework for Modal Dependent Type Theories (recording)

  Tutorial 6, Felix Wellen: Differential Cohesive HoTT, (recording)

• Dan Licata, Synthetic Mathematics in Modal Dependent Type Theories, notes for tutorial at Types, Homotopy Theory and Verification, 2018 (pdf, pdf)

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:

• Mitchell Riley, Eric Finster, Daniel Licata, Synthetic Spectra via a Monadic and Comonadic Modality (arXiv:2102.04099)

category: people