natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
There are in general two ways to define a dependent type theory:
One approach assumes a single separate type judgment and defines types via the single type judgment.
A second approach assumes an infinite number of universe levels and then defines an infinite number of type universes and, in the case for Coquand universes, type judgments indexed by , whereby types are then terms of the universes for Russell universes or identified with terms of the universes for Coquand universes via judgmental isomorphisms.
These two ways to define a dependent type theory leads to two different ways to make a dependent type theory impredicative. We assume throughout that there are some notion of dependent sum types, dependent product types, and identity types/path types.
For dependent type theories in the first sense, an impredicative dependent type theory is a dependent type theory with a type of all propositions defined via natural deduction inference rules. These dependent type theories are higher-order logics and are the internal logics of (the -categorical analogues of) elementary toposes. In general, (the -categorical analogues of) elementary toposes do not have any object classifiers.
For dependent type theories in the second sense, an impredicative dependent type theory is a dependent type theory which has the propositional resizing axiom. These impredicative dependent type theories are stronger than the other notion of impredicative dependent type theory since these are the internal logics of -categories with an infinite number of inaccessible object classifiers.
Created on August 20, 2024 at 16:48:05. See the history of this page for a list of all contributions to it.