nLab cofiber type

Definition

In dependent type theory with identity types, function types, and dependent function types, given a function $f:A \to B$, the cofiber type or cofibre type of $f$ is the higher inductive type generated by

• a term $y:\mathrm{cofiber}_{A, B}(f)$

• a function $i:B \to \mathrm{cofiber}_{A, B}(f)$

• a dependent function

  $$\mathrm{glue}:\prod_{x:A} i(f(x)) =_{\mathrm{cofiber}_{A, B}(f)} y$$

In essence, the cofiber type takes the image of the function $f:A \to B$ and makes it contractible, but leaves the rest of the codomain untouched.

Examples

• The cofiber type of the unique function out of the empty type to any type $B$ is the type $B + 1$.

• The cofiber type of a function out of the unit type to any type $B$ is equivalent to $B$.

See also

• cofiber, homotopy cofiber
• pushout type
• fiber type
• cone type

References

• Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Program, Institute for Advanced Study, 2013. (web, pdf)