\module Category.Meta

Structure Identity Principle

sip proves univalence for categories. The type of objects must extend BaseSet and the Hom-set must extend SetHom with properties only.