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
Just as one could define an internal logic, such as first order logic, higher order logic, or geometric logic in a (1,1)-category with sufficient structure, in a (2,1)-category, one should be able to define an internal set theory.
Defining a set theory internal to a (1,1)-category is not possible, unless one is talking about material set theories such as ZFC, because any groupoid or category internal to an ambient (1,1)-category is necessarily a strict groupoid or category, which violates the principle of equivalence and is thus evil. Instead, in order to construct an internal set theory, an internal notion of weak category is needed.
The basic ideas of the internal set theory induced by a given category C are:
the objects $A$ of $C$ are regarded as collections of things of a given type $A$
the morphisms $A\rightarrow B$ of $C$ are regarded as terms of type $B$ containing a free variable of type $A$ (i.e. in a context $x:A$)
A faithful morphism $F:A \rightarrow B$ is regarded as a set family of sets by thinking of it as the discrete collection of all those things of type $B$ for which the type $A$ is inhabited. $B$ is regarded as an index set. If $B$ is a terminal object $*$ in $C$, then $A$ and $F$ are equivalent as discrete objects and are regarded as sets.
Set theoretic operations are implemented by universal constructions on discrete objects.
The singleton is a terminal discrete object and a (2,1)-generator.
The Cartesian product is a (2,1)-product of discrete objects
The solution set? of a set-theoretic equation is a (2,1)-pullback of discrete objects
The disjoint union is a disjoint and (2,1)-pullback stable (2,1)-coproduct of discrete objects.
and so on.
Created on February 28, 2021 at 11:53:05. See the history of this page for a list of all contributions to it.