Algebraic Type Theory, Part 1: Martin-L\"of algebras
Category Theory
2025-05-19 v1 Logic
Abstract
A new algebraic treatment of dependent type theory is proposed using ideas derived from topos theory and algebraic set theory.
Cite
@article{arxiv.2505.10761,
title = {Algebraic Type Theory, Part 1: Martin-L\"of algebras},
author = {Steve Awodey},
journal= {arXiv preprint arXiv:2505.10761},
year = {2025}
}
Comments
In memory of Phil Scott, friend and mentor