School of Computer Science
University of Birmingham
Friday, 26 May 2017, 16:00 (note the unusual weekday and time!)
Cybernetica Bldg (Akadeemia tee 21B), room CYB-101
Slides from the talk [pdf]
Abstract: We exhibit infinite types X that have a procedure (Π(p:X →2).(Π(x:X).p(x)=0)+(Σ(x:X).p(x)=1)). Among them, several are ordinals (sets X equipped with transitive, well-founded, extensional relations) and the above procedure finds minimal witnesses when they exist. That is, this class of ordinals satisfies that every detachable, non-empty subset has a minimal element. As an example, we exhibit such a searchable ordinal dominating ε0, although it is possible to get much higher searchable ordinals indeed, which we sketch. This requires either assuming that p is extensional wrt to a setoid structure on X, or else having function extensionality, as in univalent type theories such as cubicaltt. An unplanned connection with the delay monad arises in this investigation.