nLab dependent pushout type

Idea

In dependent type theory, the binary pushout type of functions $f:A \to B$ and $g:A \to C$ is the higher inductive type $B \sqcup_{A}^{f, g} C$ generated by functions

$$\mathrm{in}_B:B \to B \sqcup_{A}^{f, g} C$$

$$\mathrm{in}_C:C \to B \sqcup_{A}^{f, g} C$$

$$\mathrm{glue}:\prod_{x:A} \mathrm{in}(f(x)) = \mathrm{in}(g(x))$$

However, by using large elimination for the boolean domain $\mathrm{bool}$ 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

$$\mathrm{ind}_\mathrm{bool}(f, g):\prod_{b:\mathrm{bool}} A \to \mathrm{rec}_\mathrm{bool}(B, C, b)$$

and the resulting binary pushout is the type

$$\mathrm{rec}_\mathrm{bool}(B, C, 0) \sqcup_{A}^{\mathrm{ind}_\mathrm{bool}(f, g, 0), \mathrm{ind}_\mathrm{bool}(f, g, 1)} \mathrm{rec}_\mathrm{bool}(B, C, 1)$$

generated by functions

$$\mathrm{in}:\prod_{b:B} \mathrm{rec}_\mathrm{bool}(B, C, b) \to (\mathrm{rec}_\mathrm{bool}(B, C, 0) \sqcup_{A}^{\mathrm{ind}_\mathrm{bool}(f, g, 0), \mathrm{ind}_\mathrm{bool}(f, g, 1)} \mathrm{rec}_\mathrm{bool}(B, C, 1))$$

$$\mathrm{glue}:\prod_{x:A} \mathrm{in}(\mathrm{ind}_\mathrm{bool}(f, g, 0, x)) = \mathrm{in}(\mathrm{ind}_\mathrm{bool}(f, g, 1, x))$$

Thus, it suffices to define the binary pushout of a boolean-indexed family of functions $f:\prod_{x:\mathrm{bool}} A \to B(x)$, which is the higher inductive type generated by the constructors

$$\mathrm{in}:\prod_{b:\mathrm{bool}} B(b) \to (B(0) \sqcup_A^{f(0), f(1)} B(1))$$

$$\mathrm{glue}:\prod_{x:A} \mathrm{in}(0, f(0, x)) = \mathrm{in}(1, f(1, x))$$

For any elements $x:A$ and $y:A$, the identity type $x = y$ is equivalent to the dependent sum type $\sum_{z:A} (x = z) \times (y = z)$, and so the glue constructor can equivalently be expressed as

$$\mathrm{glue}:\prod_{x:A} \sum_{z:B(0) \sqcup_A^{f(0), f(1)} B(1)} (\mathrm{in}(0, f(0, x)) = z) \times (\mathrm{in}(1, f(1, x) = z))$$

By induction on the booleans, this is equivalently

$$\mathrm{glue}:\prod_{x:A} \sum_{z:B(0) \sqcup_A^{f(0), f(1)} B(1)} \prod_{b:\mathrm{bool}} \mathrm{in}(b, f(b, x)) = z$$

which by the type theoretic axiom of choice is equivalently

$$\mathrm{glue}:\sum_{C:A \to (B(0) \sqcup_A^{f(0), f(1)} B(1))} \prod_{x:A} \prod_{b:\mathrm{bool}} \mathrm{in}(b, f(b, x)) = C(x)$$

Unwrapping the dependent sum type, there are now three constructors for the binary pushout of a boolean-indexed family of functions $f:\prod_{x:\mathrm{bool}} A \to B(x)$:

$$\mathrm{in}:\prod_{b:\mathrm{bool}} B(b) \to (B(0) \sqcup_A^{f(0), f(1)} B(1))$$

$$\mathrm{gluehubs}:A \to (B(0) \sqcup_A^{f(0), f(1)} B(1))$$

$$\mathrm{gluespokes}:\prod_{x:A} \prod_{b:\mathrm{bool}} \mathrm{in}(b, f(b, x)) = \mathrm{gluehubs}(x)$$

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 $A$, which are also known as wide pushouts in category theory.

Definition

As a higher inductive type

Given a type $A$, an index type $I$, a family of codomains $B(i)$ indexed by $i:I$, and a family of functions $f:\prod_{i:I} A \to B(i)$, the dependent pushout type or wide pushout type of $(A, I, B, f)$ is the higher inductive type $\bigsqcup_{x:I}^{A, f} B(x)$ generated by the constructors

$$\mathrm{in}:\prod_{i:I} B(i) \to \bigsqcup_{x:I}^{A, f} B(x)$$

$$\mathrm{gluehubs}:A \to \bigsqcup_{x:I}^{A, f} B(x)$$

$$\mathrm{gluespokes}:\prod_{x:A} \prod_{i:I} \mathrm{in}(i, f(i, x)) = \mathrm{gluehubs}(x)$$

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:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash I \; \mathrm{type} \quad \Gamma, x:I \vdash B(x) \; \mathrm{type} \quad \Gamma, x:I, z:A \vdash f(x, z):B(x)}{\Gamma \vdash \mathrm{pushout}(A, I, x.B, x z.f) \; \mathrm{type}}$$

term introduction rules:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash I \; \mathrm{type} \quad \Gamma, x:I \vdash B(x) \; \mathrm{type} \quad \Gamma, x:I, z:A \vdash f(x, z):B(x)}{\Gamma, x:I, y:B(x) \vdash \mathrm{in}(x, y):\mathrm{pushout}(A, I, x.B, x z.f) \; \mathrm{type}}$$

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash I \; \mathrm{type} \quad \Gamma, x:I \vdash B(x) \; \mathrm{type} \quad \Gamma, x:I, z:A \vdash f(x, z):B(x)}{\Gamma, z:A \vdash \mathrm{gluehubs}(z):\mathrm{pushout}(A, I, x.B, x z.f) \; \mathrm{type}}$$

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash I \; \mathrm{type} \quad \Gamma, x:I \vdash B(x) \; \mathrm{type} \quad \Gamma, x:I, z:A \vdash f(x, z):B(x)}{\Gamma, z:A, x:I \vdash \mathrm{gluespokes}(z, x):\mathrm{in}(x, f(x, z)) =_{\mathrm{pushout}(A, I, x.B, x z.f)} \mathrm{gluehubs}(z) \; \mathrm{type}}$$

term elimination rule:

$$\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash I \; \mathrm{type} \quad \Gamma, x:I \vdash B(x) \; \mathrm{type} \quad \Gamma, x:I, z:A \vdash f(x, z):B(x) \\ \Gamma, w:\mathrm{pushout}(A, I, x.B, x z.f) \vdash C(w) \; \mathrm{type} \\ \Gamma, x:I, y:B(x) \vdash g(x, y):C(\mathrm{in}(x, y)) \quad \Gamma, z:A \vdash h(z):C(\mathrm{gluehubs}(z)) \\ \Gamma, z:A, x:I \vdash s(z, x):g(x, f(x, z)) =_{C}^{\mathrm{gluespokes}(z, x)} h(z) \end{array} }{\Gamma, w:\mathrm{pushout}(A, I, x.B, x z.f) \vdash \mathrm{ind}_{(A, I, x.B, x z.f)}^{w.C}(x y.g, z.h, z x.s, w):C(w)}$$

computation rules:

$$\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash I \; \mathrm{type} \quad \Gamma, x:I \vdash B(x) \; \mathrm{type} \quad \Gamma, x:I, z:A \vdash f(x, z):B(x) \\ \Gamma, w:\mathrm{pushout}(A, I, x.B, x z.f) \vdash C(w) \; \mathrm{type} \\ \Gamma, x:I, y:B(x) \vdash g(x, y):C(\mathrm{in}(x, y)) \quad \Gamma, z:A \vdash h(z):C(\mathrm{gluehubs}(z)) \\ \Gamma, z:A, x:I \vdash s(z, x):g(x, f(x, z)) =_{C}^{\mathrm{gluespokes}(z, x)} h(z) \end{array} }{\Gamma, x:I, y:B(x) \vdash \mathrm{ind}_{(A, I, x.B, x z.f)}^{w.C}(x y.g, z.h, z x.s, \mathrm{in}(x, y)) \equiv g(x, y):C(\mathrm{in}(x, y))}$$

$$\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash I \; \mathrm{type} \quad \Gamma, x:I \vdash B(x) \; \mathrm{type} \quad \Gamma, x:I, z:A \vdash f(x, z):B(x) \\ \Gamma, w:\mathrm{pushout}(A, I, x.B, x z.f) \vdash C(w) \; \mathrm{type} \\ \Gamma, x:I, y:B(x) \vdash g(x, y):C(\mathrm{in}(x, y)) \quad \Gamma, z:A \vdash h(z):C(\mathrm{gluehubs}(z)) \\ \Gamma, z:A, x:I \vdash s(z, x):g(x, f(x, z)) =_{C}^{\mathrm{gluespokes}(z, x)} h(z) \end{array} }{\Gamma, z:A \vdash \mathrm{ind}_{(A, I, x.B, x z.f)}^{w.C}(x y.g, z.h, z x.s, \mathrm{gluehubs}(z)) \equiv h(z):C(\mathrm{gluehubs}(z))}$$

$$\frac{ \begin{array}{c} \Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash I \; \mathrm{type} \quad \Gamma, x:I \vdash B(x) \; \mathrm{type} \quad \Gamma, x:I, z:A \vdash f(x, z):B(x) \\ \Gamma, w:\mathrm{pushout}(A, I, x.B, x z.f) \vdash C(w) \; \mathrm{type} \\ \Gamma, x:I, y:B(x) \vdash g(x, y):C(\mathrm{in}(x, y)) \quad \Gamma, z:A \vdash h(z):C(\mathrm{gluehubs}(z)) \\ \Gamma, z:A, x:I \vdash s(z, x):g(x, f(x, z)) =_{C}^{\mathrm{gluespokes}(z, x)} h(z) \end{array} }{\Gamma, z:A, x:I \vdash \mathrm{apd}_{\mathrm{ind}_{(A, I, x.B, x z.f)}^{w.C}(x y.g, z.h, z x.s)}(\mathrm{gluespokes}(z, x)) \equiv s(z, x):g(x, f(x, z)) =_{C}^{\mathrm{gluespokes}(z, x)} h(z)}$$

Here:

• “$x =_A y$” denotes the identity type of elements $x:A$ and $y:A$

• “$x \equiv y:A$ denotes judgmental equality of $x:A$ and $y:A$

• “$\mathrm{apd}_{f}$” denotes dependent function application to identifications.

Properties

Descent and large elimination

The descent for the dependent pushout type $\mathrm{pushout}_{A, I, x:I.B(x)}(f)$ states that given any type family $x:I, y:B(x) \vdash C(x, y)$, any type family $w:A \vdash D(w)$, and any family of equivalences of types

$$w:A, x:I \vdash e(w, x):C(x, f(x, w)) \simeq D(w)$$

one can construct a type family $z:\mathrm{pushout}_{A, I, x:I.B(x)}(f) \vdash \mathrm{descFam}_{\mathrm{pushout}_{A, I, x:I.B(x)}(f)}^{C, D}(e, z)$ with families of equivalences of types

$$x:I, y:B(x) \vdash \mathrm{descEquiv}_{\mathrm{pushout}_{A, I, x:I.B(x)}(f)}^C(x, y):\mathrm{descFam}_{\mathrm{pushout}_{A, I, x:I.B(x)}(f)}^{C, D}(e, \mathrm{in}(x, y)) \simeq C(x, y)$$

$$w:A \vdash \mathrm{descEquiv}_{\mathrm{pushout}_{A, I, x:I.B(x)}(f)}^D(w):\mathrm{descFam}_{\mathrm{pushout}_{A, I, x:I.B(x)}(f)}^{C, D}(e, \mathrm{gluehubs}(w)) \simeq D(w)$$

and families of identifications

$$w:A, x:I \vdash \mathrm{descEquiv}_{\mathrm{pushout}_{A, I, x:I.B(x)}(f)}(e, w, x):\mathrm{descEquiv}_{\mathrm{pushout}_{A, I, x:I.B(x)}(f)}^C(x, y)^{-1} \circ \mathrm{transport}_{\mathrm{descFam}_{\mathrm{pushout}_{A, I, x:I.B(x)}(f)}^{C, D}(e)}(\mathrm{gluespokes}(w, x)) \circ \mathrm{descEquiv}_{\mathrm{pushout}_{A, I, x:I.B(x)}(f)}^D(w) =_{C(x, f(x, w)) \simeq D(w)} e(w, x)$$

or families of judgmental equality of terms

$$w:A, x:I \vdash \mathrm{descEquiv}_{\mathrm{pushout}_{A, I, x:I.B(x)}(f)}^C(x, y)^{-1} \circ \mathrm{transport}_{\mathrm{descFam}_{\mathrm{pushout}_{A, I, x:I.B(x)}(f)}^{C, D}(e)}(\mathrm{gluespokes}(w, x)) \circ \mathrm{descEquiv}_{\mathrm{pushout}_{A, I, x:I.B(x)}(f)}^D(w) \equiv e(w, x):C(x, f(x, w)) \simeq D(w)$$

Large elimination for dependent pushout types strengthens the equivalences of types in descent to judgmental equality of types

$$x:I, y:B(x) \vdash \mathrm{descFam}_{\mathrm{pushout}_{A, I, x:I.B(x)}(f)}^{C, D}(e, \mathrm{in}(x, y)) \equiv C(x, y)$$

$$w:A \vdash \mathrm{descFam}_{\mathrm{pushout}_{A, I, x:I.B(x)}(f)}^{C, D}(e, \mathrm{gluehubs}(w)) \equiv D(w)$$

and comes with families of identifications

$$w:A, x:I \vdash \mathrm{descEquiv}_{\mathrm{pushout}_{A, I, x:I.B(x)}(f)}(e, w, x):\mathrm{transport}_{\mathrm{descFam}_{\mathrm{pushout}_{A, I, x:I.B(x)}(f)}^{C, D}(e)}(\mathrm{gluespokes}(w, x)) =_{C(x, f(x, w)) \simeq D(w)} e(w, x)$$

or families of judgmental equality of terms

$$w:A, x:I \vdash \mathrm{transport}_{\mathrm{descFam}_{\mathrm{pushout}_{A, I, x:I.B(x)}(f)}^{C, D}(e)}(\mathrm{gluespokes}(w, x)) \equiv e(w, x):C(x, f(x, w)) \simeq D(w)$$

Examples

• The positive dependent sum type of a family of types $B(x)$ indexed by $x:A$ is the dependent pushout type of the family of unique functions from the empty type to each $B(x)$.

• The union of a family of subtypes of a type $A$ is given by the dependent pushout of the dependent pullback of the embeddings into $A$.

• The existential quantification of a family of mere propositions $P(x)$ indexed by $x:A$ is the dependent pushout of the $A$-indexed family of functions $\lambda f:\prod_{x:A} P(x).f(x)$ from the dependent product type $\prod_{x:A} P(x)$ to the type $P(x)$.

• Binary pushout types are boolean-indexed dependent pushout types.

• When the family of codomains $B(x)$ indexed by $x:I$ is a constant family of types, then the dependent pushout type are called dependent coequalizer types or wide coequalizer types.

Related concepts

• dependent sum type
• dependent pullback type
• pushout type
• wide pushout