Contents
Idea
In dependent type theory, given types and , an anafunction is a type family which comes with a family of witnesses
that for each element , the dependent sum type is a contractible type.
A dependent anafunction is like such an anafunction but where we allow to also depend on .
Definition
In dependent type theory (homotopy type theory), given a type and a type family , a dependent anafunction is a type family which comes with a family of witnesses
that for each element , the dependent sum type is a contractible type.
Properties
The principle of unique choice holds in dependent type theory, which means that given any dependent anafunction , there is a dependent function .
Dependent function types 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 .
See also