Type theory MOC

-types

-types, also known as dependent function types or dependent products, are motivated in several ways:

  1. -types internalize hypothetical judgements.
  2. -types generalize binary products to a product of a family of types indexed by another type.
  3. -types generalize functions so that the codomain can depend on the input.
  4. -types correspond to spaces of sections.
  5. -types correspond to universal quantification over elements of some type.

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

corresponds to a section

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

Meta-well-typed

To show that is meta-well-typed, we show that both terms have the claimed type. First note,

and by ^P2, . On the other hand,

Now ^P2 gives , and ^P1 gives , so the types agree.

To see that is meta-well-typed, note

where is conversion along the equality

which follows from ^P1 and .

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 . Translation directly into inference rules gives us almost exactly those given above, except that would look more like

with the naturality rule

and the judgemental equality rules

These are however more awkward to use since they restrict the shape of contexts. The rules presented above are derivable from these by defining :

Proof

The derivation

gives .

Noting that by ^P1 and ^P2, the derivation

gives .

The derivation

gives .

Noting by ^P1, the derivation

gives .

#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. ↩