added pointer to
(gentle exposition for complete lay readers)
]]>added pointer to:
added pointer to:
added pointer to:
added pointer to:
These references are discussed in this section at contextual category aka categorical model of dependent type theory.
]]>adding sources regarding algebraic formulations of dependent type theory
Anonymous
]]>Added reference
The link to the Agda tutorial at dependent type theory is broken.
]]>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”.
]]>