Showing math.CTShow all
3 papers · 1 filter
math.CT2024
Generalized Chevalley criteria in simplicial homotopy type theory
Jonathan Weinberger
We provide a generalized treatment of (co)cartesian arrows, fibrations, and functors. Compared to the classical conditions, the endpoint inclusions get replaced by arbitrary shape…
math.CT2024
On a fibrational construction for optics, lenses, and Dialectica categories
Matteo Capucci, Bruno Gavranović, Abdullah Malik +2
Categories of lenses/optics and Dialectica categories are both comprised of bidirectional morphisms of basically the same form. In this work we show how they can be considered a sp…
math.CT2024
Smooth and Proper Maps
Mathieu Anel, Jonathan Weinberger
This is an expository note explaining how the geometric notions of local connectedness and properness are related to the -type and -type constructors of dependent type theory…