nLab
pushout type
Redirected from "pushout types".
Contents
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 homotopy type theory , a homotopy pushout type is a kind of higher inductive type whose categorical semantics is that of homotopy pushouts .
Definition
As a higher inductive type
The (homotopy) pushout of a span A ← f C → g B A \xleftarrow{f} C \xrightarrow{g} B is the higher inductive type A ⊔ f ; g C B A \sqcup^{C}_{f ; g} B (or A ⊔ C B A \sqcup^C B ) generated by:
a function inl : A → A ⊔ C B inl : A \to A \sqcup^{C} B
a function inr : B → A ⊔ C B inr : B \to A \sqcup^{C} B
for each c : C c:C a path glue ( c ) : inl ( f ( c ) ) = inr ( g ( c ) ) glue(c) : inl (f (c)) = inr (g( c))
In Coq pseudocode:
Inductive hpushout {A B C : Type} (f : A -> B) (g : A -> C) : Type :=
| inl : B -> hpushout f g
| inr : C -> hpushout f g
| glue : forall (a : A), inl (f a) == inr (g a).
Inference rules
Explicitly, this means that the inference rules for pushout types are as follows (where we now label terms as shown in the following diagram):
type formation rule :
X , Y , Y ′ : Type ; f : X → Y , f ′ : X → Y ′ | | | | Y ⊔ X Y ′ : Type
\frac{
\begin{array}{l}
X,\, Y,\, Y^' \,\colon\, Type
\;;
\;\;
f \,\colon\, X \to Y
\;,
\;\;
f^' \,\colon\, X \to Y^'
\mathclap{\phantom{\vert_{\vert}}}
\end{array}
}
{
\mathclap{\phantom{\vert^{\vert}}}
Y \underset{X}{\sqcup} Y^'
\,\colon\,
Type
}
term introduction rules :
y : Y | | | | cpr ( y ) : Y ⊔ X Y ′ y ′ : Y ′ | | | | cpr ′ ( y ′ ) : Y ⊔ X Y ′ x : X | | | | hmt ( x ) : Id ( Y ⊔ X Y ′ ) ( cpr ( f ( x ) ) , cpr ′ ( f ′ ( x ) ) )
\frac{
y \,\colon\, Y
\mathclap{\phantom{\vert_{\vert}}}
}{
\mathclap{\phantom{\vert^{\vert}}}
cpr(y)
\,\colon\,
Y \underset{X}{\sqcup} Y^'
}
\;\;\;\;\;\;\;\;\;
\frac{
y^' \,\colon\, Y^'
\mathclap{\phantom{\vert_{\vert}}}
}{
\mathclap{\phantom{\vert^{\vert}}}
cpr^'(y^')
\,\colon\,
Y \underset{X}{\sqcup} Y^'
}
\;\;\;\;\;\;\;\;\;
\frac{
x \,\colon\, X
\mathclap{\phantom{\vert}}
}{
\mathclap{\phantom{\vert^{\vert^{\vert}}}}
hmt(x)
\,\colon\,
Id_{\big(Y \underset{X}{\sqcup} Y^'\big)}
\Big(
cpr\big(f(x)\big)
,\,
cpr^'\big(f^'(x)\big)
\Big)
}
term elimination rule :
y ^ : Y ⊔ X Y ′ ⊢ P ( y ^ ) : Type ; cpr P : ∏ y : Y P ( cpr ( y ) ) ; cpr P ′ : ∏ y ′ : Y ′ P ( cpr ′ ( y ′ ) ) ; hmt P : ∏ x : X Id P ( cpr ′ ( f ′ ( x ) ) ) ( hmt ( x ) * ( cpr P ( f ( x ) ) ) , cpr P ′ ( f ′ ( x ) ) ) | | ind ( P , cpr P , cpr P ′ , hmt P ) : ∏ y ^ : Y ⊔ X Y ′ P ( y ^ )
\frac{
\begin{array}{l}
\hat{y}
\,\colon\,
Y \underset{X}{\sqcup} Y^'
\;\vdash\;
P(\hat{y})
\,\colon\,
Type
\;;
\\
cpr_P
\,\colon\,
\underset{ y \colon Y }{\prod}
P\big(
cpr(y)
\big)
\;;
\;\;
cpr^'_P
\,\colon\,
\underset{ y^' \colon Y^' }{\prod}
P\big(
cpr^'(y^')
\big)
\;;
\\
hmt_P
\,\colon\,
\underset{x \colon X}{\prod}
Id_{P\Big( cpr^'\big(f^'(x)\big) \Big)}
\bigg(
hmt(x)_\ast
\Big(
cpr_P\big(
f(x)
\big)
\Big)
,\,
cpr^'_P\big(
f^'(x)
\big)
\bigg)
\end{array}
}{
\mathclap{\phantom{\vert^{\vert}}}
ind_{\big(P,\, cpr_P,\,cpr^'_P,\,hmt_P\big)}
\,\colon\,
\underset{
\hat{y} \,\colon\, Y \underset{X}{\sqcup} Y^'
}{\prod}
\,
P(\hat{y})
}
computation rules :
y ^ : Y ⊔ X Y ′ ⊢ P ( y ^ ) : Type ; cpr P : ∏ y : Y P ( cpr ′ ( y ) ) ; cpr P ′ : ∏ y ′ : Y ′ P ( cpr ′ ( y ′ ) ) ; hmt P : ∏ x : X Id P ( x ) ( hmt ( x ) * ( cpr P ( f ( x ) ) ) , cpr P ′ ( cpr ′ ( x ) ) ) | | ind ( P , cpr P , cpr P ′ , hmt P ) ∘ cpr = cpr P ; | | ind ( P , cpr P , cpr P ′ , hmt P ) ∘ cpr ′ = cpr P ′ ; happly ( ind ( P , cpr P , cpr P ′ , hmt P ) ) ∘ hmt = hmt P
\frac{
\begin{array}{l}
\hat{y}
\,\colon\,
Y \underset{X}{\sqcup} Y^'
\;\vdash\;
P(\hat{y})
\,\colon\,
Type
\;;
\\
cpr_P
\,\colon\,
\underset{ y \colon Y }{\prod}
P\big(
cpr^'(y)
\big)
\;;
\;\;
cpr^'_P
\,\colon\,
\underset{ y^' \colon Y^' }{\prod}
P\big(
cpr^'(y^')
\big)
\;;
\\
hmt_P
\,\colon\,
\underset{x \colon X}{\prod}
Id_{P(x)}
\bigg(
hmt(x)_\ast
\Big(
cpr_P\big(
f(x)
\big)
\Big)
,\,
cpr^'_P\big(
cpr^'(x)
\big)
\bigg)
\end{array}
}{
\begin{array}{rlc}
\mathclap{\phantom{\vert^{\vert}}}
ind_{\big(P,\, cpr_P,\,cpr^'_P,\,hmt_P\big)}
\,\circ\,
cpr
&=&
cpr_P
\;;
\\
\mathclap{\phantom{\vert^{\vert}}}
ind_{\big(P,\, cpr_P,\,cpr^'_P,\,hmt_P\big)}
\,\circ\,
cpr^'
&=&
cpr^'_P
\;;
\\
happly_{\big(
ind_{\big(P,\, cpr_P,\,cpr^'_P,\,hmt_P\big)}
\big)}
\,\circ\,
hmt
&=&
hmt_P
\end{array}
}
Here:
Examples
See also
References
Early discussion of the idea of homotopy pushouts as higher inductive types :
Many references on higher inductive types mention pushout types and highlight their categorical semantics, but skip type-theoretic details, e.g.:
The full inference rules are stated in:
as well as in section 6 of:
See also:
Formalization in the Coq proof assistant :
Last revised on February 10, 2024 at 22:32:10.
See the history of this page for a list of all contributions to it.