nLab
Bishop set

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

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
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
conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idemponent) 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

Bishop sets

Idea

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

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.

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

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

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
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
conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idemponent) 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

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

See also

Revised on March 1, 2014 04:53:22 by Urs Schreiber (89.204.135.214)