All Questions
Tagged with category-theory cubical-type-theory
2
questions
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
27
votes
2
answers
879
views
What is Artin gluing, and how is it useful in proving meta-theoretic properties?
I came across this notion in several places, especially in recent papers that establish important meta-theoretic properties of type theories like CuTT. The entry in nLab focuses on the geometric ...
- 4,025