5 papers
Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory
Hakon Robbestad Gylterud, Elisabeth Stenholm, Niccolò Veltri
Non-well-founded material sets have been modelled in Martin-Löf type theory by Lindström using setoids. In this paper we construct models of non-wellfounded material sets in Homo…
Doctrinal Semantics of Directed First-Order Logic
Andrea Laretto, Fosco Loregian, Niccolò Veltri
We present a first-order logic equipped with an "asymmetric" directed notion of equality, which can be thought of as rewrites between terms, allowing for types to be interpreted as…
Di- is for Directed: First-Order Directed Type Theory via Dinaturality
Andrea Laretto, Fosco Loregian, Niccolò Veltri
We show how dinaturality plays a central role in the interpretation of directed type theory where types are interpreted as (1-)categories and directed equality is represented by $\…
Derivatives for Containers in Univalent Foundations
Philipp Joram, Niccolò Veltri
Containers conveniently represent a wide class of inductive data types. Their derivatives compute representations of types of one-hole contexts, useful for implementing tree-traver…
Monoid Structures on Indexed Containers
Michele De Pascalis, Tarmo Uustalu, Niccolò Veltrì
Containers represent a wide class of type constructions relevant for functional programming and (co)inductive reasoning. Indexed containers generalize this notion to better fit the…