35 citations · 105 across the 17 of their papers we have counts for
Showing 2019Show all
2 papers · 1 filter
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…
cs.LO2019★ 4 cited
A type theory for cartesian closed bicategories
Marcelo Fiore, Philip Saville
We construct an internal language for cartesian closed bicategories. Precisely, we introduce a type theory modelling the structure of a cartesian closed bicategory and show that it…