  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 define structures on sets. We develop the syntax,
semantics and deductive system for such a logic, which we call first-order
logic with isomorphism ($\text{FOL}_{\cong}$). The syntax of
$\text{FOL}_{\cong}$ extends $\text{FOL}_{=}$ in two ways. First, by
incorporating into its signatures a notion of dependent sorts along the lines
of Makkai's FOLDS as well as a notion of an $h$-level of each sort. Second, by
specifying three new logical sorts within these signatures: isomorphism sorts,
reflexivity predicates and transport structure. The semantics for
$\text{FOL}_{\cong}$ are then defined in homotopy type theory with the
isomorphism sorts interpreted as identity types, reflexivity predicates as
relations picking out the trivial path, and transport structure as transport
along a path. We then define a deductive system $\mathcal{D}_{\cong}$ for
$\text{FOL}_{\cong}$ that encodes the sense in which the inhabitants of
isomorphism sorts really do behave like isomorphisms and prove soundness of the
rules of $\mathcal{D}_{\cong}$ with respect to its homotopy semantics. Finally,
as an application, we prove that precategories, strict categories and univalent
categories are axiomatizable in $\text{FOL}_{\cong}$.
