nLab Bishop set

Idea

A Bishop set is a notion of set in constructive mathematics, commonly used in Bishop's constructive mathematics (cf. constructive analysis).

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.

Formalization in type theory

Formally, the definition of Bishop set presumes some prior notion of “collection” (the elements) and “relation” (the equality) that can be put together. These collections are sometimes called presets, and can be formalized in various ways. In particular, presets generally lack operations such as quotients and even subsets.

One of the most common approaches is to use type theory, where the collections are simply types. Note that this is a different approach to the use of type theory in foundations of mathematics than that of, for instance, homotopy type theory — in the latter, type theory is enriched with operations on types such as quotients, enabling them to be the basic set-like objects out of which mathematics is built; while in the Bishop-set approach one defines “sets” as types equipped with extra structure, so that the sets have quotient-type operations even though the types do not. There is an analogy to the construction of the exact completion of a category, which has quotients even if the original category does not.

Frequently, the type theories used for this purpose do not even have a separate notion of “relation” or “proposition”, and thus the untruncated propositions as types interpretation is used for the equivalence relations in a Bishop set. That is, one has a type $X:Type$ of elements and a type family $R:X\to X \to Type$ with witnesses that it is “reflexive, symmetric, and transitive”, but nothing prevents $R(x,y)$ from having more than one element. (If the type theory has identity types, one could demand that $R$ consist of h-propositions, but at least historically this is not often done.) This means that categorically, the Bishop sets are most like the ex/lex completion of the category of types — although the morphisms in the ex/lex completion are defined as a quotient in the ambient set theory, whereas the morphisms between Bishop sets simply form another Bishop set.

For example, see (Palmgren05) for an exposition and (Coquand-Spiwack, section 3) for a brief list of the axioms.

In the context of type theory Bishop sets are also called setoids.

Properties

The predicative topos of Bishop sets

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:

Theorem

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).

Related concepts

• setoid, quotient type

• constructive mathematics

• ETCS

algebraic structure	oidification
magma	magmoid
pointed magma with an endofunction	setoid/Bishop set
unital magma	unital magmoid
quasigroup	quasigroupoid
loop	loopoid
semigroup	semicategory
monoid	category
anti-involutive monoid	dagger category
associative quasigroup	associative quasigroupoid
group	groupoid
flexible magma	flexible magmoid
alternative magma	alternative magmoid
absorption monoid	absorption category
cancellative monoid	cancellative category
rig	CMon-enriched category
nonunital ring	Ab-enriched semicategory
nonassociative ring	Ab-enriched unital magmoid
ring	ringoid
nonassociative algebra	linear magmoid
nonassociative unital algebra	unital linear magmoid
nonunital algebra	linear semicategory
associative unital algebra	linear category
C-star algebra	C-star category
differential algebra	differential algebroid
flexible algebra	flexible linear magmoid
alternative algebra	alternative linear magmoid
Lie algebra	Lie algebroid
monoidal poset	2-poset
strict monoidal groupoid?	strict (2,1)-category
strict 2-group	strict 2-groupoid
strict monoidal category	strict 2-category
monoidal groupoid	(2,1)-category
2-group	2-groupoid/bigroupoid
monoidal category	2-category/bicategory

References

The original texts, with focus on constructive analysis:

• Errett Bishop: Foundations of Constructive Analysis, McGraw-Hill (1967)

• Errett Bishop, Douglas Bridges: Constructive Analysis, Grundlehren der mathematischen Wissenschaften 279, Springer (1985) [doi:10.1007/978-3-642-61667-9]

Discussion of Bishop sets — under the name setoids — as categorical semantics for dependent type theory:

• Martin Hofmann, Extensional concepts in intensional type theory, Ph.D. thesis, University of Edinburgh (1995), Distinguished Dissertations, Springer (1997) [ECS-LFCS-95-327, pdf, doi:10.1007/978-1-4471-0963-1]

Review and relation to ETCS:

• Erik Palmgren, Bishop’s set theory (2005) [pdf, pdf]

• Erik Palmgren, Constructivist and Structuralist Foundations: Bishop’s and Lawvere’s Theories of Sets, Annals of Pure and Applied Logic 163 10 (2012) 1384-1399 (2009) [doi:10.1016/j.apal.2012.01.011, arXiv:1201.6272]

• Erik Palmgren, Bishop-style constructive mathematics in type theory – a tutorial (2013) [pdf, pdf]

The term “Bishop set” and their formalization in type theory (essentially as for setoids, but not mentioning this term) appears (in a context of formalization of homological algebra) in:

• Thierry Coquand, Arnaud Spiwack, section 3 of: Towards constructive homological algebra in type theory, in: Towards Mechanized Mathematical Assistants. MKM Calculemus 2007, Lecture Notes in Computer Science 4573 Springer (2007) [doi:10.1007/978-3-540-73086-6_4, pdf]

Some of the text above is taken from this section.

The predicative topos formed by Bishop sets in type theory is discussed in

• Ieke Moerdijk, Erik Palmgren, Wellfounded trees in categories. Ann. Pure Appl. Logic, 104(1-3):189–218, (2000)

• Benno van den Berg, Predicative toposes (arXiv:1207.0959)

A formalization of constructive set theory in terms of setoids in intensional type theory coded in Coq is discussed in

• Erik Palmgren, Olov Wilander, Constructing categories of setoids in type theory, (pdf, Coq)

See also

• UF-IAS-2012, On the setoid model of type theory (video)

• UF-IAS-2012, Setoid model of type theory formalized

• Discussion on categorical aspects of the setoid construction.