Introduces TTS, a dependent type theory replacing global canonical composition with regime-indexed indiscernibility and constructive apartness, proving conservativity, provenance, no-fork-from-empty, and persistence of forks under refinement.
Title resolution pending
3 Pith papers cite this work. Polarity classification is still indexing.
3
Pith papers citing it
verdicts
UNVERDICTED 3representative citing papers
Cocartesian fibrations are defined in synthetic simplicial type theory with closure properties proved using a novel equivalence between LARI adjunctions and initial sections.
Presents directed first-order logic with asymmetric equality as relative left adjoint, polarity system for variances, and sound-complete semantics via directed doctrines; classical fragment complete in preorders.
citing papers explorer
-
A Type Theory of Sense: Witnessed Choice in Stratified Semantic Spaces
Introduces TTS, a dependent type theory replacing global canonical composition with regime-indexed indiscernibility and constructive apartness, proving conservativity, provenance, no-fork-from-empty, and persistence of forks under refinement.
-
Fibrations in Directed Type Theory
Cocartesian fibrations are defined in synthetic simplicial type theory with closure properties proved using a novel equivalence between LARI adjunctions and initial sections.
-
Doctrinal Semantics of Directed First-Order Logic
Presents directed first-order logic with asymmetric equality as relative left adjoint, polarity system for variances, and sound-complete semantics via directed doctrines; classical fragment complete in preorders.