Type theory MOC

-types

-types, also known as dependent pair types or dependent sums, are motivated in several ways:

  1. -types internalize context extension.
  2. -types generize binary coproducts to a coproduct of a family of types indexed by another type.
  3. -types generalize binary products so that the type of the right element can depend on the type of the left input.
  4. -types correspond to total spaces of a fibration.
  5. -types correspond to existential quantification over elements of some type.

The core idea is that given a type family (fibration) , a term

corresponds to a pair of terms and , and vice versa.

Standard presentation

Here we give a formal presentation of -types in the cartesian calculus of substitutions, following Principles of dependent type theory. #m/def/type The formation, introduction, and elimination rules are given by1

while we also have the substitution naturality rules2

and judgemental equality rules for β-computation and η-unicity

Internalizing judgemental structure

In terms of Internalizing judgemental structure, we can formalize the correspondence described in the core idea with an operation

natural in with a family of bijections

also natural in .

#state/tidy | #lang/en | #SemBr

Footnotes

  1. For brevity and laziness, the premisses of the formation rule will be considered presuppositions. ↩

  2. Where we invoke Substitution extension by a type. ↩