推出 (一种余极限) [推出]

定义

推出是以 $$ \bullet \leftarrow \bullet \rightarrow \bullet $$ 为指标范畴的余极限, 是拉回的对偶.

同伦类型论

在同伦类型论中, 对于类型 $X,Y$ 以及 $Q\colon X\to Y \to\mathsf{Type}$, 定义推出 $X \sqcup_Q Y$ 为如下高阶归纳类型:

  • $\mathsf{left} \colon X \to X\sqcup_Q Y$
  • $\mathsf{right} \colon Y \to X\sqcup_Q Y$
  • $\mathsf{glue}\colon \prod_{x\colon X}\prod_{y\colon Y} Q(x,y) \to (\mathsf{left}\,x =\mathsf{right}\,y)$