Redirected from "Pi-types".
Dependent product types
Dependent product types
Idea
In dependent type theory, a dependent product type , for a dependent type is the type of “dependently typed functions” assigning to each an element of .
In a model of the type theory in categorical semantics, this is a dependent product. In set theory, it is an element of an indexed product.
It includes function types as the special case when is not dependent on , product types as a special case when is the type of Booleans, and dependent sequence types as a special case when is the natural numbers type.
Overview
Definition
Like any type constructor in type theory, a dependent product type is specified by rules saying when we can introduce it as a type, how to construct terms of that type, how to use or “eliminate” terms of that type, and how to compute when we combine the constructors with the eliminators.
The type formation rule for dependent product type is:
As a negative type
Dependent product types are almost always defined as negative types. In this presentation, primacy is given to the eliminators. The natural eliminator of a dependent product type says that we can apply it to any input:
The constructor is then determined as usual for a negative type: to construct a term of , we have to specify how it behaves when applied to any input. In other words, we should have a term of type containing a free variable . This yields the usual “-abstraction” constructor:
The beta-reduction rule is the obvious one, saying that when we evaluate a -abstraction, we do it by substituting for the bound variable.
If we want an eta-conversion rule, the natural one says that every dependently typed function is a -abstraction:
As a positive type
It is also possible to present dependent product types as a positive type. However, this requires a stronger metatheory, such as a logical framework. We use the same constructor (-abstraction), but now the eliminator says that to define an operation using a function, it suffices to say what to do in the case that that function is a lambda abstraction.
This rule cannot be formulated in the usual presentation of type theory, since it involves a “higher-order judgment”: the context of the term involves a “term of type containing a free variable ”. However, it is possible to make sense of it. In dependent type theory, we need additionally to allow to depend on .
The natural -reduction rule for this eliminator is
and its -conversion rule looks something like
Here is a term containing a free variable of type . By substituting for , we obtain a term of type which depends on “a term containing a free variable ”. We then apply the positive eliminator at , and the -rule says that this can be computed by just substituting for in .
Positive versus negative
As usual, the positive and negative formulations are equivalent in a suitable sense. They have the same constructor, while we can formulate the eliminators in terms of each other:
The conversion rules also correspond.
In dependent type theory, this definition of only gives us a properly typed dependent eliminator if the negative dependent product type satisfies -conversion. As usual, if it satisfies propositional eta-conversion then we can transport along that instead—and conversely, the dependent eliminator allows us to prove propositional -conversion. This is the content of Propositions 3.5, 3.6, and 3.7 in (Garner).
Dependent product types a la Russell and a la Tarski
In dependent type theory, there are two different ways to interpret the term :
-
is literally a family of terms in the family of types indexed by
-
is a term representation for a family of terms in the family of types indexed by
This situation is similar to how there are two notions of type universe where small types of a universe are interpreted a la Russell, literally as types, or a la Tarski, as a term representation of types. Thus, in analogy to type universes, we can refer to dependent product types a la Russell and function types a la Tarski.
Dependent product types a la Russell and a la Tarski are expressed respectively via the elimination rule of function types:
- given type and the type family and an element , one could form the family of terms
- given type and the type family one could form the family of terms
Dependent product types a la Tarski corresponds to the notion of dependent product in category theory where the dependent product literally comes with a morphism in the slice category , but dependent product types a la Russell are the one most commonly used in dependent type theory.
The conversion rules for dependent product types a la Russell are as follows:
and the conversion rules for dependent product types a la Tarski are as follows:
For the rest of the article we shall assume the use of dependent product types a la Russell.
Weak and strict dependent product types
In dependent type theory, weak dependent product types are dependent product types for which the computation rules (-conversion) and uniqueness rules (-conversion) are propositional rather than judgmental:
Weak dependent product types appear in weak type theories.
This contrasts with strict dependent product types which use judgmental computation and uniqueness rules:
Strict dependent product types appear in most dependent type theories such as Martin-Löf type theory, observational type theory, and cubical type theory.
For strict dependent product types, the judgmental computation and uniqueness rules automatically imply the propositional computation and uniqueness rules, as by the rules for judgmental equality and identity types, judgmental equality of two terms always implies propositional equality of the two terms.
In terms of function types
Given a dependent type theory with function types, dependent sum types, and identity types, the dependent product type of a type family indexed by can be defined as the type of functions from to the dependent sum type such that the composite of with the first projection function is the identity function on
The underlying family of elements is then given by the composite of with the second projection function of the dependent sum type:
Similarly, given a family of elements , one could construct the function
such that given , . By lambda abstraction, one has
and so the dependent function is given by
One also has which is the associated computation rule for dependent function types. Meanwhile, from the judgmental -conversion rules for negative dependent sum types and function types, one could prove the judgmental -conversion rule for dependent function types. Given
one has
As types of dependent anafunctions
In the same way that one could define equivalence types as types of one-to-one correspondences and function types as types of anafunctions, one could define dependent function types as types of dependent anafunctions. This requires both identity types and heterogeneous identity types being defined first, which we shall write as and respectively for , , , , and . We use Agda notation for dependent function types rather than the dependent product type notation or in this section.
Rules for dependent function types
By the rules for dependent pair types and dependent function types, one could derive that
which is precisely the statement that is a dependent anafunction for all dependent functions .
Properties
Universal property of dependent product types
The universal property of dependent product types states that for all types and type families , there is a family of functions
such that for any other type and family of functions , there is a unique function such that
If there is a type universe , then one could wrap this into a single axiom.
Typal computation and uniqueness rules
The typal computation rule for function types is provable from the other four typal type formers of function types. Given type , type family and dependent function , we have, by the elimination rule and the introduction rule, a dependent function , which by the uniqueness rules of dependent product types are equal to each other
By the inductively defined function which takes identifications between dependent functions to homotopies between dependent functions, we have that
which is the typal computation rule for dependent function types.
Typal congruence rules
These are called typal congruence rules because they are the analogue of the judgmental congruence rules which use identity types and weak equivalence types instead of judgmental equality.
Strict dependent product types
Since dependent product types are negative types, we first present the typal congruence rule for the elimination rule of dependent product types
Theorem
Given a type and a type family , dependent functions and and an identification there are families of identifications .
Proof
We simply define the dependent function to be happly, which is inductively defined on identity types.
The next is the typal congruence rule for the introduction rule of dependent function types. However, unlike the case for the other two rules, one needs dependent function extensionality.
Theorem
Assuming dependent function extensionality, given type and family of types , families of elements and , and families of identifications , there is a identification
Proof
By the computation rule of strict dependent function types, there are families of judgmental equalities
Thus, by the structural rules of judgmental equality, there are families of identifications
and by -abstraction, one gets the dependent function
By dependent function extensionality, there is an equivalence of types
which yields an identification
We define
Finally, we present the typal congruence rule for the formation rule of function types, which relies upon the previous two results. The theorem and proof differs significantly whether one uses definitional isomorphisms or some notion of equivalences of types.
Using definitional isomorphisms
Theorem
Given types and and type families , and definitional isomorphisms and dependent function consisting of a family of definitional isomorphisms, there is a definitional isomorphism
Proof
Since for definitional isomorphism , we have judgmental equalities and , so we do not need to transport across identifications. Instead, we define the function
by
and the inverse function by
Now it suffices to construct judgmental equalities
from where it implies that is thus a definitional isomorphism.
By definition, we have
and by the computation rules of strict dependent product types, we have
and because is a definitional isomorphism, we have
By the congruence rules for substitution of judgmental equality, we have
Since for all each is also a strict equality, we have
by the congruence rules for substitution of judgmental equality, we have
and by the uniqueness rule of dependent function types we have
thus by the transitive rule for judgmental equality we have
for all
Similarly, by definition, we have
and by the computation rules for strict dependent product types, we have
and because is a definitional isomorphism, we have
By the congruence rules for substitution of judgmental equality, we have
Since for all each is also a strict equality, we have
by the congruence rules for substitution of judgmental equality, we have
and by the uniqueness rule of dependent function types we have
thus by the transitive rule for judgmental equality we have
for all .
Since we have functions
and families of judgmental equalities
we could form the definitional isomorphism
By a common abuse of notation we denote the definitional isomorphism by the same name as the underlying function ; thus we have
Using weak equivalences of types
Theorem
Given types and and type families , and equivalence and dependent function , there is an equivalence
Proof
We define the function
by
and the inverse function by
where the equivalence has families of identifications
witnessing that is a section and retraction of respectively.
Now it suffices to construct families of identifications
from where it implies that has a coherent inverse and contractible fibers and is thus an equivalence of types.
By definition,
By the computation rules of strict dependent function types, there is a family of judgmental equalities
and thus by the structural rules of judgmental equalities and the judgmental congruence rules for dependent function types, a judgmental equality
In addition, the equivalence has the coherence condition
So we have the family of elements
and by applying the function
across one gets the family of identifications
in type
From the family of elements
one could define the family of dependent functions
This means by applying the above dependent function to , , , , , and , one gets the family of identifications
in type
By the judgmental computation rules of identity types, we have , which means that we have
and we have
Thus by concatenation we have identification
in type
and by application of to the above identification, we have
in type
Similarly, The family of equivalences
has a family of identifications
witnessing that is a retraction of for each .
By substituting in for we get the family of identifications
and thus the family of identifications
in type
and the dependent function
in type
By dependent function extensionality, we get the identification
in type
and since we defined
we have
We can define the witness that is a retraction of as
Similarly, by definition,
By the computation rules of strict dependent function types, there is a family of judgmental equalities
and thus by the structural rules of judgmental equalities and the judgmental congruence rules for dependent function types, a judgmental equality
From the family of elements
one could define the family of dependent functions
This means by applying the above dependent function to , , , , , and , one gets the family of identifications
in type
By the judgmental computation rules of identity types, we have
Similarly, The family of equivalences
has a family of identifications
witnessing that is a section of for each .
By substituting in for and in for in the above expression we get the family of identifications
and by transport across we get
By concatenation of identifications we get
in type
and by -abstraction we get
in type
By dependent function extensionality, we get the identification
in type
and since we defined
we have
We can define the witness that is a section of as
Since we have functions
and families of identifications
we could form the equivalence
By a common abuse of notation we denote the equivalence by the same name as the underlying function ; thus we have
Weak dependent product types
Theorem
Assuming dependent function extensionality, given types and and type families and and equivalences and dependent function of equivalences , there is an equivalence
Since dependent function types are negative types, we first present the typal congruence rule for the elimination rule of dependent function types
Theorem
Given a type and a type family , dependent functions and and an identification there are families of identifications .
Proof
We simply define the dependent function to be happly, which is inductively defined on identity types.
The next is the typal congruence rule for the uniqueness rule of dependent function types.
Theorem
For weak dependent product types with dependent function
given
-
a type
-
a type family
-
dependent functions and
-
an identification ,
there is a family of identifications
The next is the typal congruence rule for the introduction rule of function types. However, unlike the case for the other two rules, one needs dependent function extensionality.
Theorem
Assuming dependent function extensionality, given a type and a type family , families of elements and , and families of identifications , there is an identification
Proof
By the computation rule of weak dependent function types, there are families of identifications
Thus, there are families of identificaitons
and by -abstraction, one gets the dependent function
By dependent function extensionality, there is an equivalence of types
which yields an identification
We define
Application in logic
In logic, dependent functions types express universal quantifications. More precisely, for a predicate on a type , under propositions as types the universal quantification is the dependent product type (or rather the bracket type of that if one wishes to force this to be of type again ).
Graph of a dependent function
Given a type and a type family , there is a function
which takes a dependent function and returns the graph of a dependent function
defined by for all . As a dependent anafunction the graph of the dependent function is represented by the identity type family
Relation to sections
A family of type is equivalently a type with a function . Then each is defined as the fiber of at element . Then the dependent product of a function is defined as the dependent product type
or equivalently, due to the type theoretic axiom of choice, as the dependent sum type
which says that is a section of . One could eliminate the use of the dependent product type entirely by using the definition of dependent product type from function types:
Categorical interpretation
In categorical semantics, the dependent product types are relative right adjoints to context extension in comprehension categories.
There is also another interpretation in category theory of the dependent product type over as the terminal -indexed wide span under , the object with a family of morphisms
such that for any other object with a family of morphisms , there exists a unique morphism such that
References
The standard rules for type-formation, term introduction/elimination and computation of dependent product type are listed for instance in part I of
Another textbook account could be found in section 2.1 of:
as well as sections 1.4 and 2.9 of:
See also:
On the categorical semantics of dependent product types as relative right adjoints to context extension in comprehension categories:
- Michael Lindgren, Dependent products as relative adjoints, Stockholm (2021) [pdf]