Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I have created a stub for dependent type theory.
This used to redirect to just type theory, but in that entry it is being escaped to Martin-Löf type theory, so clearly either it should redirect there or have a separate entry. I guess a separate entry is better, since there is dependent type theory that is not of Martin-Löf “type”.
The link to the Agda tutorial at dependent type theory is broken.
Added reference
1 to 3 of 3