Encoding Dependently-Typed Constructions into Simple Type Theory

on YouTube ↗22m

" summary

Claims an encoding of most of Lean’s dependent constructions into Isabelle/HOL by representing type families as a single set-valued function X : N → set, using locales to pack operations and axioms, and choosing a non‑extensional function-space encoding to keep automation fast. Builds a formalisation of strict omega‑categories (pasting‑diagram model encoded as rooted trees), reports that automation (notably Sledgehammer) proves many lemmas, notes loss of universe polymorphism and the need for faithfulness checks before tackling weak infinity categories.

AI-written summary · about

" chapters (11)

1. 0:00Start
2. 0:29Dependent vs simple types
3. 3:19The Isabelle module system
4. 5:00Motivation
5. 6:21Basics of n-categories
6. 7:30A first definition
7. 12:51Function extensionality
8. 15:19The strict w-category of pasting diagrams
9. 17:47How to encode a pasting diagram
10. 18:14Dependent types simplified
11. 19:09Summary