A Higher Structure Identity Principle
arXiv:1702.07776
Abstract
We prove a Structure Identity Principle for theories defined on types of -level 3 by defining a general notion of saturation for a large class of structures definable in the Univalent Foundations.
25 pages