-
arXiv:2102.06275 [pdf, ps, other]
The Univalence Principle
Abstract: The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined in a non-algebraic and space-based style, as well as models of higher-order theories such as topological spaces. In particular, we formulate a general definition of… ▽ More
Submitted 29 August, 2022; v1 submitted 11 February, 2021; originally announced February 2021.
Comments: A short version of this book is available as arXiv:2004.06572. v2: added references and some details on morphisms of premonoidal categories; v3: added proof that exo-nat is sharp if cofibrant, improved presentation following advice from referee
MSC Class: 18N99; 03B38; 03G30; 55U35
-
arXiv:2004.06572 [pdf, ps, other]
A Higher Structure Identity Principle
Abstract: The ordinary Structure Identity Principle states that any property of set-level structures (e.g., posets, groups, rings, fields) definable in Univalent Foundations is invariant under isomorphism: more specifically, identifications of structures coincide with isomorphisms. We prove a version of this principle for a wide range of higher-categorical structures, adapting FOLDS-signatures to specify a… ▽ More
Submitted 23 June, 2020; v1 submitted 14 April, 2020; originally announced April 2020.
Comments: Long version of publication in LICS 2020 (DOI: 10.1145/3373718.3394755); v2: added sections "Axioms and Theories" and "Version History", other minor changes; v3: added examples
-
arXiv:1707.07339 [pdf, ps, other]
Finite Inverse Categories as Signatures
Abstract: We define a simple dependent type theory and prove that its well-formed types correspond exactly to finite inverse categories.
Submitted 23 July, 2017; originally announced July 2017.
Comments: 11 pages
MSC Class: 03B70; 03F50; 18C99
-
arXiv:1702.07776 [pdf, ps, other]
A Higher Structure Identity Principle
Abstract: We prove a Structure Identity Principle for theories defined on types of $h$-level 3 by defining a general notion of saturation for a large class of structures definable in the Univalent Foundations.
Submitted 24 February, 2017; originally announced February 2017.
Comments: 25 pages
MSC Class: 03G99; 03B15; 03B22; 03C99
-
arXiv:1603.03092 [pdf, ps, other]
First-Order Logic with Isomorphism
Abstract: 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… ▽ More
Submitted 25 September, 2017; v1 submitted 9 March, 2016; originally announced March 2016.
Comments: 62 pages; Major revision incorporating referee's comments, improving exposition, clarifying results, constructions and proofs, and extending the system to also include transport structure
MSC Class: 03G99; 03B15; 03B22; 03C99
-
arXiv:1507.02302 [pdf, ps, other]
A Syntactic Characterization of Morita Equivalence
Abstract: We characterize Morita equivalence of theories in the sense of Johnstone in terms of a new syntactic notion of a common definitional extension developed by Barrett and Halvorson for cartesian, regular, coherent, geometric and first-order theories. This provides a purely syntactic characterization of the relation between two theories that have equivalent categories of models naturally in any Grothe… ▽ More
Submitted 8 July, 2015; originally announced July 2015.