5 citations · 11 across the 11 of their papers we have counts for
3 papers · 1 filter
Free constructions for comprehension categories
Francesco Dagnino, Jacopo Emmenegger, Andrea Giusto
Jacobs comprehension categories subsume a large class of categorical models of type dependency, supporting also the description of morphisms between types. We study the relationshi…
Categorical models of subtyping
Greta Coraglia, Jacopo Emmenegger
Most categorical models for dependent types have traditionally been heavily set based: contexts form a category, and for each we have a set of types in said context -- and for each…
The solutions to single-variable polynomials, implemented and verified in Lean
Nicholas Dyson, Benedikt Ahrens, Jacopo Emmenegger
In this work, we describe our experience in learning the use of a computer proof assistant - specifically, Lean - from scratch, through proving formulae for the solutions of polyno…