Algebraic Type Theory, Part 1: Martin-L\"of algebras

TL;DR

This paper introduces an algebraic framework for dependent type theory inspired by topos theory and algebraic set theory, aiming to provide a new foundational perspective.

Contribution

It presents a novel algebraic approach to dependent type theory, connecting it with topos theory and algebraic set theory.

Findings

Develops a new algebraic formulation of dependent type theory

Establishes connections between type theory and topos-theoretic concepts

Provides foundational insights for future algebraic treatments of type theories

Abstract

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