@article{gratzer-2024-the, title={The category of iterative sets in homotopy type theory and univalent foundations}, volume={34}, ISSN={1469-8072}, url={http://dx.doi.org/10.1017/s0960129524000288}, DOI={10.1017/s0960129524000288}, number={9}, journal={Mathematical Structures in Computer Science}, publisher={Cambridge University Press (CUP)}, author={Gratzer, Daniel and Gylterud, Håkon Robbestad and Mörtberg, Anders and Stenholm, Elisabeth}, year={2024}, month=Oct, pages={945–970} }