paper

Algebraic Type Theory, Part 1: Martin-Löf algebras

arXiv:2505.10761

Abstract

A new algebraic treatment of dependent type theory is proposed using ideas derived from topos theory and algebraic set theory.

In memory of Phil Scott, friend and mentor