Redirected from "bijective-on-objects functors".
This entry currently contains mistakes, see the discussion page here.
Contents
Definition
There are two different fundamental theorems of identity types, depending on whether identity types are defined with plain identity induction or with based identity induction.
With identity induction
The fundamental theorem of identity types states that given a type , a type family and a family of functions
the following conditions are equivalent:
-
For each the dependent sum type of the type family is a contractible type.
-
There is a family of equivalences
-
is an identity system.
-
For each and , the function is an equivalence of types
-
is a retraction
-
with the function satisfies the universal property of the unary sum of .
With based identity induction
The fundamental theorem of identity types states that given a type , an element , a type family and a family of functions
the following conditions are equivalent:
-
The dependent sum type of the type family is a contractible type.
-
There is a family of equivalences
-
equipped with is an identity system.
-
For each , the function is an equivalence of types
-
For each , is a retraction
-
For each , with the function satisfies the universal property of the unary sum of .
Proofs that the conditions are the same
Proof that conditions 1 and 2 are the same
Suppose the equivalence type used in the second definition is a weak equivalence type. It is possible to show that definitions 1 and 2 are the same.
Definition 1 implies definition 2, because both and are contractible types, there is a weak equivalences of types
Thus, there is a family of functions
indexed by , defined by
and by currying this is the same as the function
defined by
Then by theorem 11.1.3 of Rijke22, since is an equivalence of types, then each is an equivalence of types for all . Thus we define to be .
Definition 2 implies definition 1, as we begin with a family of weak equivalences
or equivalently
We can get a weak equivalences
by defining
The type is always contractible; this means the type is contractible as well, since the two types are equivalent to each other. Thus, one could construct a witnesses
Proof that conditions 2 and 4 are the same
Suppose the equivalence type used in the second definition is a weak equivalence type. Then definitions 2 and 3 are the same because given any type and , there is a equivalence
Thus, in one direction, we define
and in the other direction, we inductively define by induction on reflexivity
Proof that condition 4 implies condition 5
Suppose that for every we have a witness that the function is an equivalence of types
For every type and , there is a family of functions
which takes a witness that is an equivalence to a quasi-inverse function of . The retraction of is represented by
Proof that condition 5 implies condition 1
This proof is adapted from Dan Licata in Licata 16:
Suppose that for every we have a function
and a family of homotopies
This exhibits as a retract of , hence as a retract of the contractible type , so there is an element
See also
References
The fundamental theorem of identity types appears in section 11.2 of
Definition 5 arises as a generalization of this proof by Dan Licata for univalent universes:
- Dan Licata, weak univalence with “beta” implies full univalence (web)