From the Sigma-type to the Grothendieck construction

TL;DR

This paper explores the correspondence between Sigma-types in Martin-Löf Type Theory and the Grothendieck construction in category theory, translating properties and axioms between these frameworks.

Contribution

It establishes a formal connection showing how properties of Sigma-types translate into categorical isomorphisms involving the Grothendieck construction, including the axiom of choice.

Findings

Equivalences in MLTT correspond to category isomorphisms

Axioms like the type-theoretic axiom of choice are reflected categorically

Associativity of Sigma-types translates into categorical properties

Abstract

We translate properties of the Sigma-type in Martin-L\"of Type Theory (MLTT) to properties of the Grothendieck construction in category theory. Namely, equivalences in MLTT that involve the Sigma-type motivate isomorphisms between corresponding categories that involve the Grothendieck construction. The type-theoretic axiom of choice and the "associativity" of the Sigma-type are the main examples of this phenomenon that are treated here.