natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
symmetric monoidal (∞,1)-category of spectra
monoid theory in algebra:
In set theory, algebraic structures such as monoids are defined as a set with additional structure and equational axioms. However, in homotopy type theory, there are two possible notions of what it means for a type to be a set, and what it means that a set has equational axioms. Traditionally in homotopy type theory, a set is defined using the identity type, where every identity type between two elements $a:A$ and $b:A$ of a type $A$ is propositionally truncated. However, equality in set theory is usually defined as an equivalence relation, and one could directly translate the equivalence relation of equality into homotopy type theory, resulting in a symmetric proset. The equational axioms of algebraic structures could similarly be defined using the equivalence relation of the symmetric proset rather than the identity type. In the context of defining monoids, this results in the notion of a monoidal symmetric proset.
In homotopy type theory, a monoidal symmetric proset is a symmetric proset $(M, \equiv_M)$ with a binary function $(-)\cdot(-):M \times M \to M$, an element $1:M$, and witnesses of associativity, left unitality, right unitality, and extensionality
A monoidal symmetric proset is univalent or a monoid if the canonical function
is an equivalence of types for all elements $a:M$ and $b:M$.
Every monoidal symmetric proset is (the delooping of) a (2, 1)-preorder? with only 1 object.
Last revised on September 22, 2022 at 19:09:09. See the history of this page for a list of all contributions to it.