2 papers
math.CT2025
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 theo…
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…