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
Given a modal operator , then a type may be called -comodal or -connected (largely now the preferred term) if (the unit type).
Since a type is called a -modal type if , being comodal is in a sense the opposite extreme of being modal.
In as far as modal operators have categorical semantics as idempotent (co-)-monads/idempotent (∞,1)-(co-)monads anti-modal types are familiar in homotopy theory as forming localizing subcategories.
for the n-truncation modality, then -comodal is indeed n-connected, by this proposition.
a comodal type for a reduction modality or infinitesimal shape modality is an anti-reduced type, is an infinitesimally thickened point.
The term “anti-modal type” appears in
Last revised on March 25, 2020 at 10:27:58. See the history of this page for a list of all contributions to it.