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 , the cofiber type or cofibre type of is the higher inductive type generated by
a term
a function
a dependent function
In essence, the cofiber type takes the image of the function 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 is the type .
The cofiber type of a function out of the unit type to any type is equivalent to .
Last revised on October 16, 2022 at 00:14:07. See the history of this page for a list of all contributions to it.