41 citations · 172 across the 17 of their papers we have counts for
4 papers · 1 filter
Quotient inductive-inductive types
Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra +2
Higher inductive types (HITs) in Homotopy Type Theory (HoTT) allow the definition of datatypes which have constructors for equalities over the defined type. HITs generalise quotien…
Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type
Thorsten Altenkirch, Nils Anders Danielsson, Nicolai Kraus
Capretta's delay monad can be used to model partial computations, but it has the "wrong" notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay m…
Notions of Anonymous Existence in Martin-Löf Type Theory
Nicolai Kraus, Martín Escardó, Thierry Coquand +1
As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-Löf type theory cannot generally be shown to be unique. Inspired by a theorem by Hedber…
Extending Homotopy Type Theory with Strict Equality
Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus
In homotopy type theory (HoTT), all constructions are necessarily stable under homotopy equivalence. This has shortcomings: for example, it is believed that it is impossible to def…