Groupoid Model of H0TT in Lean 4

Bibliography

Awo17

Steve Awodey. Natural models of homotopy type theory, 2017.

Awo23

Steve Awodey. On hofmann-streicher universes, 2023.

Hof95

Martin Hofmann. Extensional concepts in intensional type theory, 1995.

HS98

Martin Hofmann and Thomas Streicher. The groupoid interpretation of type theory. In Twenty-five years of constructive type theory (Venice, 1995), volume 36 of Oxford Logic Guides, pages 83–111. Oxford Univ. Press, New York, 1998.

Joy

André Joyal. Model structures on cat. https://ncatlab.org/joyalscatlab/published/Model+structures+on+Cat.