From the Sigma-type to the Grothendieck construction
Category Theory
2021-09-10 v1
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.
Cite
@article{arxiv.2109.04239,
title = {From the Sigma-type to the Grothendieck construction},
author = {Iosif Petrakis},
journal= {arXiv preprint arXiv:2109.04239},
year = {2021}
}
Comments
14 pages