Di- is for Directed: First-Order Directed Type Theory via Dinaturality
summary
Proposes a first-order directed type theory interpreting types as categories, terms as functors, predicates as dipresheaves, and entailments as dinatural transformations; uses a syntactic restriction on the directed J-rule that recovers reflexivity, transitivity, congruence and transport but blocks symmetry; treats quantifiers as ends and coends and gives logical proofs of (co)Yoneda, Kan adjointness, presheaf exponentials and Fubini; main theorems are machine-checked with an Agda formalization and artifacts are available and reusable.
AI-written summary · about
chapters (20)
- 0:00Introduction
- 0:21Motivation for directed type theory
- 1:04Category theory meets first-order logic
- 3:30From groupoids to directed categories
- 5:16Types as categories terms as functors
- 7:02Solving polarity with D-naturality
- 8:02Directed type theory overview
- 9:26Judgments for types and terms
- 10:08Formulas and directed quantifiers
- 12:13Variable usage natural and dashial
- 13:37Dinatural transformations and composition
- 14:39Rules for directed equality
- 16:25Symmetry not derivable
- 17:07Computational content and J rule
- 18:10Dependent J and unitality proofs
- 19:15Naturality from directed equality
- 20:17Logical rules for connectives
- 20:59Proving category theory theorems
- 22:04Future work and limitations
- 22:46Conclusion and Q&A
related talks
53mIntroduction to Intuitionistic Type Theory
30mA Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized
52mType Theory and its Meaning Explanations
54mCategory Theory Through Functional Programming (part 3/3)
02h 24mCategory Theory Track
49mFinite functional programming via graded effects and relevance types
31mAlgebraic Data Types, Categorically
25mLinear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl)