15 citations · 21 across the 3 of their papers we have counts for
3 papers
math.LO2021★ 2 cited
Constructing Initial Algebras Using Inflationary Iteration
Andrew M. Pitts, S. C. Steenkamp
An old theorem of Adámek constructs initial algebras for sufficiently cocontinuous endofunctors via transfinite iteration over ordinals in classical set theory. We prove a new vers…
cs.LO2021★ 15 cited
Quotients, inductive types, and quotient inductive types
Marcelo P. Fiore, Andrew M. Pitts, S. C. Steenkamp
This paper introduces an expressive class of indexed quotient-inductive types, called QWI types, within the framework of constructive type theory. They are initial algebras for ind…
cs.LO2019★ 4 cited
Constructing Infinitary Quotient-Inductive Types
Marcelo Fiore, Andrew M. Pitts, S. C. Steenkamp
This paper introduces an expressive class of quotient-inductive types, called QW-types. We show that in dependent type theory with uniqueness of identity proofs, even the infinitar…