New answers tagged type-theory
5
Definitional equality is the same as equality in the metatheory. It works exactly the same way as in 1-category theory. If I have a category $\mathbb{C}$ and some morphisms $f,g : \mathbb{C}(A, B)$, I write $f = g$ for their equality, where $=$ is a metatheoretical relation. I can assume a family structure on $\mathbb{C}$ to get a CwF, plus assume some type ...
2
Definitional equality is essentially a syntactic notion of equality, not witnessed by a term in the type theory: when two types or terms are definitionally equal, we are saying that they are precisely the same. Therefore, definitional equality of types is interpreted as equality of objects, and definitional equality of terms is interpreted as equality of ...
0
I think that you've asked two slightly different questions which are both worth answering. Other answers are good for the question in the title, but I want to focus on the word "fundamental" in your second question.
For large fragments of most mainstream programming languages, there exists a native type theory (discussed at nCafé: 1 2 3) which ...
4
To me, type theory bridges programming with models and proof theories. In particular, I can use category theory to think about programming languages when the underlying type theory has a categorical model (e.g. the intuitionistic type theory by Martin Löf).
On the other hand, type theory to programming is like (point-set) topology to analysis -- it gives you ...
3
"Types are the leaven of computer programming; they make it digestible." Robin Milner
1
Example usage of $\top$'s eliminator: to prove $\Pi_{x:\top} x=_1 \star$ (this is a propositional equality), the uniqueness principle of $\top$.
With the eliminator, you can prove it by eliminating the parameter $x$. This is a theorem that must take an instance of $\top$. A constant map won't prove the theorem.
If you change the type checker to make it turn ...
Top 50 recent answers are included
