All Questions
Tagged with category-theory type-theory
9
questions
1
vote
1
answer
85
views
Is every type-theoretic function ℕ → A extensionally equal to one written in terms of the ℕ-eliminator
In Category Theory the Natural Numbers object ℕ has the universal mapping-out property that tells us how to build arrows out of ℕ into an arbitrary object A. But it doesn't say that every arrow ...
- 345
5
votes
1
answer
471
views
Semantics of type theory
There are many tools regarding the semantics of type theory. On one hand, we may organize the structure of substitutions explicitly, resulting in notions such as CwFs, CwAs, natural models, display ...
- 4,025
3
votes
1
answer
153
views
Stacks versus universes
This is a vague question, and I apologize in advance for it. I do not need a definite answer, I am happy to just get some general ideas.
An elementary topos can model higher order logic over a ...
- 722
9
votes
1
answer
180
views
Interpretation of dependent types: Coherence
I have trouble understanding precisely how dependent type theories are intepreted in categories (in the most simple case, for example in a locally cartesian closed category). I know that a type in ...
- 722
10
votes
0
answers
187
views
Is there a proof assistant (or an embedding) for the (co)end calculus?
A Higher-Order Calculus for Categories describes a system where you can conveniently perform manipulations with categories, functors, Yoneda embeddings etc. An example of the rules is: $$\frac{\Gamma ,...
- 4,025
18
votes
2
answers
562
views
What are the motivations for different variants of categorical models of dependent type?
I am new to the categorical semantics for dependent type theories, so it is surprising for me to see nLab introduces so many variants of categorical models, including comprehension categories, display ...
- 429
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
6
votes
0
answers
114
views
Is every logical theory embeddable in a dependently typed extensional type theory?
In category theory by the Yoneda embedding every category $\mathcal{C}$ is a subcategory of a category of presheafs $[\mathcal{C}^{\text{op}}, \text{Set}]$. Every category of presheafs is a topos and ...
- 2,868
5
votes
0
answers
95
views
What is the relation of $\lambda^\to$ and $\lambda^{\to\times}$ to cartesian closed categories?
I am learning about the categorical semantics of type theory. I've written some preliminary results in Agda. In particular, I partially proved that the contexts and substitutions of simply-typed ...
- 4,025