Redirected from "coequalizer types".
Contents
Contents
Idea
The instantiation of a coequalizer as a type in dependent type theory.
Definition
In dependent type theory, given types and and functions and , the coequalizer type or coequaliser type of and is a higher inductive type . There are two different way to define the coequalizer type. The first way states that is generated by the constructors
The second way states that is generated by
Induction and recursion principles
The recursion principle for coequalizer types says that given a type together with
- a function
- a dependent function
there exists a function such that
- for all , , and
- for all , , , , and ,
Similarly, the induction principle says that given a type family indexed by together with
- a dependent function
- a dependent function
there exists a dependent function such that
- for all , , and
- for all , , , , and ,
Properties
Relation to W-suspensions
W-suspensions could be constructed as the coequalizer type of the left and middle dependent pair projections and of the dependent pair type , both of which have domain and codomain :
Alternatively, given two parallel functions and , the coequalizer of and could be defined as the W-suspension generated by the graph defined by the family of dependent sum types
Examples
- The sum type of a type with itself is the coequalizer of two copies of the unique function from the empty type to .
- The circle type is the coequalizer of any two endofunctions and on a contractible type .
- The interval type is the coequalizer of the constant functions with value and from any contractible type to the boolean domain.
- More generally, the suspension of a type is the coequalizer of the constant functions with value and from to the boolean domain.
- The cyclic group of order for natural number is the coequalizer of the constant functions with value and from any contractible type to the natural numbers type.
- The pushout of a span and is the coequalizer of the composite functions and , each with domain and codomain the sum type :
Propositional truncation
The propositional truncation of a h-set is the set truncation of the coequalizer of the two product projection functions and of the product type
See also
References