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 $\bigcirc$, then a type $X$ may be called $\bigcirc$-comodal or $\bigcirc$-connected (largely now the preferred term) if $\bigcirc X \simeq \ast$ (the unit type).
Since a type $Y$ is called a $\bigcirc$-modal type if $\bigcirc Y \simeq Y$, 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 $\bigcirc = n \coloneqq \tau_n$ the n-truncation modality, then $n$-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 06:27:58. See the history of this page for a list of all contributions to it.