Constructive characterizations of bar subsets
From MaRDI portal
Publication:866574
DOI10.1016/j.apal.2006.10.003zbMath1154.03039MaRDI QIDQ866574
Publication date: 14 February 2007
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.apal.2006.10.003
constructive mathematics; type theory; formal topology; bar induction; constructive ordinals; bar theorem; generalized inductive definitions
54A05: Topological spaces and generalizations (closure spaces, etc.)
06D22: Frames, locales
03F65: Other constructive mathematics
Related Items
Cites Work
- Type-theoretic interpretation of iterated, strictly positive inductive definitions
- On the formal points of the formal topology of the binary tree
- Inductively generated formal topologies.
- A set constructor for inductive sets in Martin-Löf's type theory
- Every countably presented formal topology is spatial, classically
- A linear category of polynomial diagrams
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item