Internal Algebraic Type Theory
This thesis brings us closer to applying computer-assisted, internal, type-theoretic reasoning to a category, with examples in the category of cubical sets, the category of groupoids, and the category of categories. The steps we make towards this general goal are both in furthering the type theoretic analysis of these examples, as well as implementing computer-assisted syntax-semantic reasoning as part of the HoTTLean project. One key component of this work is the consideration of new exponentiability conditions with respect to a class of maps in a category, and the development of polynomial…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2608.00095
curl -X POST /api/v1/records/arxiv/2608.00095/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2608.00095/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'