nLab Bishop set

Bishop sets

Context

Constructivism, Realizability, Computability

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction setinternal homfunction type
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian productdependent productdependent product type
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijectionisomorphism/adjoint equivalenceequivalence of types
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Internal categories

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axiom

Removing axioms

Bishop sets

Idea

A Bishop set is a notion of set in constructive mathematics, commonly used in Bishop's 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 AA to a set BB 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 ff which assigns an element f(a)f(a) of BB to each given element aa of AA”. This notion of routine is left informal but must “afford an explicit, finite, mechanical reduction of the procedure for constructing f(a)f(a) to the procedure for constructing aa.”

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:TypeX:Type of elements and a type family R:XXTypeR:X\to X \to Type with witnesses that it is “reflexive, symmetric, and transitive”, but nothing prevents R(x,y)R(x,y) from having more than one element. (If the type theory has identity types, one could demand that RR 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 a Bishop set is sometimes called a setoid.

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

algebraic structureoidification
truth valuepreorder
magmamagmoid
pointed magma with an endofunctionsetoid/Bishop set
unital magmaunital magmoid
quasigroupquasigroupoid
looploopoid
semigroupsemicategory
monoidcategory
anti-involutive monoiddagger category
associative quasigroupassociative quasigroupoid
groupgroupoid
flexible magmaflexible magmoid
alternative magmaalternative magmoid
absorption monoidabsorption category
cancellative monoidcancellative category
rigCMon-enriched category
nonunital ringAb-enriched semicategory
nonassociative ringAb-enriched unital magmoid
ringringoid
nonassociative algebralinear magmoid
nonassociative unital algebraunital linear magmoid
nonunital algebralinear semicategory
associative unital algebralinear category
C-star algebraC-star category
differential algebradifferential algebroid
flexible algebraflexible linear magmoid
alternative algebraalternative linear magmoid
Lie algebraLie algebroid
monoidal poset2-poset
strict monoidal groupoid?strict (2,1)-category
strict 2-groupstrict 2-groupoid
strict monoidal categorystrict 2-category
monoidal groupoid(2,1)-category
2-group2-groupoid/bigroupoid
monoidal category2-category/bicategory

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction setinternal homfunction type
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian productdependent productdependent product type
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijectionisomorphism/adjoint equivalenceequivalence of types
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

References

The original publication is

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

in the context of constructive analysis. A detailed discussion is in

  • M. Hofmann, Extensional constructs in Intensional Type theory, Springer (1997)

Reviews include

  • Erik Palmgren, Constructivist and Structuralist Foundations: Bishop’s and Lawvere’s Theories of Sets (2009) (web)

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

Last revised on September 21, 2022 at 01:48:30. See the history of this page for a list of all contributions to it.