A General Construction of Strict Models in HoTT
Homotopy type theory (HoTT) provides a natural setting for studying the metatheory of type theory, as it comes with additional extensionality principles compared to ordinary Martin-Löf type theory. In particular, it is especially suitable for developing semantics of type theory, where one distinguishes two kinds of models: strict models, which give us sound interpretations, and pseudomodels. Pseudomodels are useful as they occur prevalently and can be turned into strict models by constructions called strictifications. However, the commonly used strictifications do not translate well to HoTT,…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2610.28370
curl -X POST /api/v1/records/arxiv/2610.28370/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2610.28370/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'