First-Order Logic with Isomorphism

Dimitris Tsementzis

The Univalent Foundations requires a logic that allows us to define structures on homotopy types, similar to how first-order logic with equality (${\text{FOL}}_{=}$) allows us to defin…