-Types in Categories of Coalgebras
arXiv:1901.06539
Abstract
We construct -types in the category of coalgebras for a cartesian comonad. It generalizes the constructions of -types in presheaf toposes and gluing toposes.
arXiv:1901.06539
We construct -types in the category of coalgebras for a cartesian comonad. It generalizes the constructions of -types in presheaf toposes and gluing toposes.