natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
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
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.
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$.
Last revised on October 16, 2022 at 00:14:07. See the history of this page for a list of all contributions to it.