All Questions
Tagged with category-theory homotopy-type-theory
3
questions
1
vote
2
answers
285
views
Formalization of a model of ∞-category in a proof assistant
I am aware of similar question in MO whose comment nicely lists zoo of possible models and only such models can be formalized. But I have not found any implementation so far which I could use or ...
- 133
11
votes
1
answer
288
views
Seven Trees in One, or How to formalize the Semiring of Types?
This is somewhat conceptual beginner's question about proof assistants.
I've been re-reading the famous Seven Trees in One / Objects of categories as complex numbers. The gist: The type $T$ of binary ...
- 213
19
votes
2
answers
1k
views
What are "fibration/cofibration" in type theory and what are their intuitions?
I keep seeing these phrasing in some proof assistants/elaborators and their issues/internal discussions (e.g. Github search results in cooltt), that seems not that related to the actual proofs/...
- 301