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 type theory, a split context is a context , where the judgments in are required to be separated from the judgments in , so that while it is possible for those in to depend on those in , the judgments in are not allowed to depend on the judgments in .
Split contexts are frequently used in modal type theories such as spatial type theory and cohesive homotopy type theory in order to make comonadic modalities work. Specifically Shulman’s real-cohesive homotopy type theory and Riley’s linear homotopy type theory use split contexts.
Last revised on May 12, 2023 at 05:25:54. See the history of this page for a list of all contributions to it.