KnowledgeBase » SEMINAR » ID = 737

Constructive Topology - A Theory of Observation

by Francisco Mota
2014

Constructive topology eschews the point-set topology point-of-view in which points are essential and observations (open sets) are collections of points. Instead, we view observation as the primitive and points are a derived notions. This way we can do topology without relying on any non-constructive principles, such as LEM, the Axiom of Choice, or the Boolean Prime Ideal theorem. This seminar is about coming up to speed with the basics of constructive topology and comparing the treatment of "observable properties" in the point-set topology vs constructive topology, as well as asking what we can do with these ideas in type theory.