Redirected from "wide pushout type".
Context
Type theory
Homotopy theory
homotopy theory, (∞,1)-category theory, homotopy type theory
flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed…
models: topological, simplicial, localic, …
see also algebraic topology
Introductions
Definitions
Paths and cylinders
Homotopy groups
Basic facts
Theorems
Contents
Idea
In dependent type theory, the binary pushout type of functions and is the higher inductive type generated by functions
However, by using large elimination for the boolean domain on the codomain of the functions and by using the induction principle for the boolean domain on the functions themselves, one has a family of functions
and the resulting binary pushout is the type
generated by functions
Thus, it suffices to define the binary pushout of a boolean-indexed family of functions , which is the higher inductive type generated by the constructors
For any elements and , the identity type is equivalent to the dependent sum type , and so the glue constructor can equivalently be expressed as
By induction on the booleans, this is equivalently
which by the type theoretic axiom of choice is equivalently
Unwrapping the dependent sum type, there are now three constructors for the binary pushout of a boolean-indexed family of functions :
By generalizing this definition of binary pushouts from the boolean domain to any arbitrary type, one gets general dependent pushouts of an arbitrary family of functions with domain , which are also known as wide pushouts in category theory.
Definition
As a higher inductive type
Given a type , an index type , a family of codomains indexed by , and a family of functions , the dependent pushout type or wide pushout type of is the higher inductive type generated by the constructors
This is an example of the hubs-and-spokes construction of higher inductive types discussed in the HoTT book, and is an non-recursive higher inductive type.
Inference rules
Explicitly, this means that the inference rules for dependent pushout types are as follows:
type formation rule:
term introduction rules:
term elimination rule:
computation rules:
Here:
Properties
Descent and large elimination
The descent for the dependent pushout type states that given any type family , any type family , and any family of equivalences of types
one can construct a type family with families of equivalences of types
and families of identifications
or families of judgmental equality of terms
Large elimination for dependent pushout types strengthens the equivalences of types in descent to judgmental equality of types
and comes with families of identifications
or families of judgmental equality of terms
Examples
-
The positive dependent sum type of a family of types indexed by is the dependent pushout type of the family of unique functions from the empty type to each .
-
The union of a family of subtypes of a type is given by the dependent pushout of the dependent pullback of the embeddings into .
-
The existential quantification of a family of mere propositions indexed by is the dependent pushout of the -indexed family of functions from the dependent product type to the type .
-
Binary pushout types are boolean-indexed dependent pushout types.
-
When the family of codomains indexed by is a constant family of types, then the dependent pushout type are called dependent coequalizer types or wide coequalizer types.