6 citations · 13 across the 4 of their papers we have counts for
6 papers
The Univalence Principle
Benedikt Ahrens, Paige Randall North, Michael Shulman +1
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,…
A Higher Structure Identity Principle
Benedikt Ahrens, Paige Randall North, Michael Shulman +1
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 und…
Finite Inverse Categories as Signatures
Dimitris Tsementzis, Matthew Weaver
We define a simple dependent type theory and prove that its well-formed types correspond exactly to finite inverse categories.
A Higher Structure Identity Principle
Dimitris Tsementzis
We prove a Structure Identity Principle for theories defined on types of -level 3 by defining a general notion of saturation for a large class of structures definable in the Uni…
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 () allows us to defin…
A Syntactic Characterization of Morita Equivalence
Dimitris Tsementzis
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 fo…