Search

• < Previous
• 1
• Next >

On Small Types in Univalent Foundations

We investigate predicative aspects of constructive univalent foundations. By predicative and constructive, we respectively mean that we do not assume Voevodsky's propositional resizing axioms or excluded middle. Our work complements existing work on predicative mathematics by exploring what cannot&nbsp;[&hellip;]