constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
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
category object in an (∞,1)-category, groupoid object
basic constructions:
strong axioms
A Bishop set is a notion of set in constructive mathematics.
In (Bishop) the notion of set is specified by stating that a set has to be given by a description of how to build elements of this set and by giving a binary relation of equality, which has to be an equivalence relation.
A function from a set $A$ to a set $B$ is then given by an operation, which is compatible with the equality (i.e. two elements which are equal in A are mapped to two elements which are equal in B), and is described as “a finite routine $f$ which assigns an element $f(a)$ of $B$ to each given element $a$ of $A$”. This notion of routine is left informal but must “afford an explicit, finite, mechanical reduction of the procedure for constructing $f(a)$ to the procedure for constructing $a$.”
These ideas have been formalized in type theory, where they serve to set up set theory in an ambient type theoretic logical framework. See Formalization in type theory below.
It is direct and natural to represent formally the notion of Bishop sets in type theory. See for instance (Palmgren05) for an exposition and (Coquand-Spiwack, section 3) for a brief list of the axioms.
In the context of type theory a Bishop set is sometimes called a setoid.
In much of set theory the category Set of all sets is a Topos. For Bishop sets formalized in type theory this is not quite the case. Instead:
The category of Bishop sets in Martin-Löf dependent type theory is a strong predicative topos.
This is (van den Berg, theorem 6.2), based on (Moerdijk-Palmgren, section 7).
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
The original publication is
in the context of constructive analysis. A detailed discussion is in
Reviews include
The formalization of Bishop set is reviewed for instance in section 3 of
(there with an eye towards further formalization of homological algebra).
Some of the text above is taken from this section.
The predicative topos formed by Bishop sets in type theory is discussed in
A formalization of constructive set theory in terms of setoids in intensional type theory coded in Coq is discussed in
See also
UF-IAS-2012, On the setoid model of type theory (video)
Discussion on categorical aspects of the setoid construction.