From the Sigma-type to the Grothendieck construction
Reviewed by Pith T0 review T1 audit T2 compute T3 formal T4 kernel pith:SXBX6NI6record.jsonopen to challenge →
classification
math.CT
keywords
sigma-typeconstructiongrothendieckinvolvemlttpropertiestheoryassociativity
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.