Papers › First-Order Logic with Isomorphism
First-Order Logic with Isomorphism
Dimitris Tsementzis
The archive published only this paper's code-link row. Authors, date and abstract are from arXiv's metadata (CC0), read from the Kaggle arXiv metadata snapshot of 2026-09-12 where its title matched the archive's; the title is the archive's.
The Univalent Foundations requires a logic that allows us to define structures on homotopy types, similar to how first-order logic with equality (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 (FOL_≅). The syntax of FOL_≅ extends 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 FOL_≅ 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 𝒟_≅ for FOL_≅ that encodes the sense in which the inhabitants of isomorphism sorts really do behave like isomorphisms and prove soundness of the rules of 𝒟_≅ with respect to its homotopy semantics. Finally, as an application, we prove that precategories, strict categories and univalent categories are axiomatizable in FOL_≅.
Code
Repository list and official/mentioned flags are the archive's, frozen 2025-07-28. Reachability, where shown, is from one Syntology probe window (2026-09-16 to 2026-09-18); repositories not probed show nothing. GitHub stars are not tracked.
Code Syntology ran Syntology
Not run by Syntology. Nothing on this page verifies that the listed code works.
Results from the paper archive 2025-07-28
No leaderboard rows for this paper in the archive.
Report a problem or propose a change · a person checks every report against the paper or source before anything changes; decisions are listed on /corrections