Related papers: Univalence and Ontic Structuralism
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…
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…
Starting from the observation that distinct notions of copying have arisen in different categorical fields (logic and computation, contrasted with quantum mechanics) this paper addresses the question of when, or whether, they may coincide.…
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…
In this paper, we explore the 'equivalence principle' (EP): roughly, statements about mathematical objects should be invariant under an appropriate notion of equivalence for the kinds of objects under consideration. In set theoretic…
There are different meanings of foundation of mathematics: philosophical, logical, and mathematical. Here foundations are considered as a theory that provides means (concepts, structures, methods etc.) for the development of whole…
I examine the debate between substantivalists and relationalists about the ontological character of spacetime and conclude it is not well posed. I argue that the so-called Hole Argument does not bear on the debate, because it provides no…
Category theory unifies mathematical concepts, aiding comparisons across structures by incorporating objects and morphisms, which capture their interactions. It has influenced areas of computer science such as automata theory, functional…
We present a generalization of the notion of an algebra norm relevant to real finite-dimensional unital associative algebras. Among other things, this leads to a novel set of algebra isomorphism invariants, some of which are computationally…
Symmetries and isomorphisms play similar conceptual roles when we consider how models represent physical situations, but they are formally distinct, as two models related by symmetries are not typically isomorphic. I offer a rigorous…
The intended model of the homotopy type theories used in Univalent Foundations is the infinity-category of homotopy types, also known as infinity-groupoids. The problem of higher structures is that of constructing the homotopy types needed…
This paper develops a categorical framework to clarify the relationship between the completeness and compactness theorems in classical first-order logic. Rather than claiming that different model constructions yield naturally isomorphic…
Starting from a Unified Field Theory (UFT) proposed previously by the author, the possible fermionic representations arising from the same spacetime are considered from the algebraic and geometrical viewpoint. We specifically demonstrate in…
We investigate two constructive approaches to defining quasi-compact and quasi-separated schemes (qcqs-schemes), namely qcqs-schemes as locally ringed lattices and as functors from rings to sets. We work in Homotopy Type Theory and…
The investigations on higher-order type theories and on the related notion of parametric polymorphism constitute the technical counterpart of the old foundational problem of the circularity (or impredicativity) of second and higher order…
We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this system, we propose a definition of "category" for which equality…
It is shown the construction of a module structure [2] with universe over a set of a particular kind of mathematical proofs, the base ring of this module will be built on a maximal consistent extension of a set of propositions, this…
Similarity in formal argumentation has recently gained attention due to its significance in problems such as argument aggregation in semantics and enthymeme decoding. While existing approaches focus on propositional logic, we address the…
In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps of presheaves. We study these in…
This is an introductory textbook to univalent mathematics and homotopy type theory, a mathematical foundation that takes advantage of the structural nature of mathematical definitions and constructions. It is common in mathematical practice…