nLab Nicola Gambino

Nicola Gambino is associate professor of mathematics at Leeds.

• website

Selected writings

On inductive types in homotopy type theory via homotopy-initial algebras over an endofunctor:

• Steve Awodey, Nicola Gambino, Kristina Sojakova, Inductive types in homotopy type theory, LICS’12: (2012) 95–104 [arXiv:1201.3898, doi:10.1109/LICS.2012.21, Coq code]

  
  

  Exposition:

  Steve Awodey, Inductive types in HoTT (Jan 2012) [blog post]

and analogously on higher inductive types:

• Steve Awodey, Nicola Gambino, Kristina Sojakova, Homotopy-initial algebras in type theory, Journal of the ACM 63 6 (2017) 1–45 [arXiv:1504.05531, doi:10.1145/3006383]

On the constructive model structure on simplicial sets:

• Nicola Gambino, Christian Sattler, Karol Szumiło, The constructive Kan-Quillen model structure: two new proofs (arXiv:1907.05394)

On Kripke-Joyal semantics and forcing in homotopy type theory:

• Steve Awodey, Nicola Gambino, Sina Hazratpour, Kripke-Joyal forcing for type theory and uniform fibrations (2021) [arXiv:2110.14576]

Related entries

• homotopy limit

• monad

• type theory, homotopy type theory

• higher inductive type, initial algebra over an endofunctor, W-types

• software verification

category: people