Shallowly embedding type theories
summary
Library in Agda implements a shallow embedding of object type theories as presheaf models parameterized by a small base category, representing contexts/types/terms as records (not inductive syntax) and providing substitutions, weakening and context extension. It already instantiates omega to get guarded recursion with an explicit later modality, loop induction, a Stream type and map that typechecks after three automated naturality proofs. A built naturality solver generates those equality proofs; automation via Agda reflection is ongoing.
AI-written summary · about
chapters (7)
- 0:00Start
- 0:13Motivation
- 2:12A bird's-eye view of the framework
- 3:27Presheaves intuitively
- 10:02Presheaf categories as models for type theory
- 13:09Concrete example: guarded recursion
- 16:02Proof by reflection for naturality
related talks
14mType-Sensitive Algebraic Macros
25mMonadic typed tactic programming by reflection
53mIntroduction to Intuitionistic Type Theory
20mA Dependent Type Theory for Meta-programming with Intensional Analysis
15mElaboration with First-Class Implicit Function Types
24mA Formalization of Opaque Definitions for a Dependent Type Theory
16mA Hoare-Logic Style Refinement Types Formalisation
23mImplementing a category-theoretic framework for typed abstract syntax