constructive set theory in nLab

+-- {: .rightHandSide}
+-- {: .toc .clickDown tabindex="0"}
### Context
#### Constructivism, Realizability, Computability
+-- {: .hide}
[[!include constructivism - contents]]
=--
#### Foundations
+-- {: .hide}
[[!include foundations - contents]]
=--
=--
=--

\tableofcontents

## Idea

Constructive set theory is [[set theory]] in the spirit of [[constructive mathematics]]. 

[[Algebraic set theory]] is a categorical presentation of such set theories.

Some more information can be found at [[ZFC]]. Perhaps this should be moved here.

## Axiom systems

There are a number of axiom systems:

### Impredicative set theories

All of these set theories can be interpreted in a [[set-level type theory]] with a [[type of all propositions]]. 

* The impredicative IZF which includes the [[power set]] or [[power object]] axiom. 
* [[SEAR|ISEAR]] - the [[allegorical set theory]] version of IZF. 
* [[ETCS|IETCSR]] - the [[categorical set theory]] version of IZF. 

### Weakly predicative set theories

All of these set theories can be interpreted in [[set-level type theory]] with no [[type of all propositions]], but with [[function types]] and [[dependent function types]]

* The variant CZF for [[predicative mathematics]]. 
* [[SEAR|CSEAR]] - the [[allegorical set theory]] version of CZF. 
* [[ETCS|CETCSR]] - the [[categorical set theory]] version of CZF. 

### Strongly predicative set theories

All of these set theories can be interpreted in [[set-level type theory]] with only dependent function types for families of [[subsingletons]]. 

* [[SEAR|PSEAR]] 

## Related concepts

* [[constructive analysis]]

* [[constructive algebraic topology]]


* [[taboo]]

## References

* {#AczelRathjen01} [[Peter Aczel]], [[Michael Rathjen]], _Notes on Constructive Set theory_, 2001 ([pdf](https://events.math.unipd.it/3wftop/pdf/AczelRathjen.pdf), [[AczelRathjenCST.pdf:file]])

See also

* Wikipedia, _[Constructive set theory](http://en.wikipedia.org/wiki/Constructive_set_theory)_

On constructive [[non-wellfounded set theory]] in [[homotopy type theory]]:

* [[Håkon Robbestad Gylterud]], [[Elisabeth Stenholm]], [[Niccolò Veltri]], *Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory* &lbrack;[arXiv:2001.06696](https://arxiv.org/abs/2001.06696)&rbrack;


[[!redirects CZF]]
[[!redirects IZF]]
[[!redirects CST]]