## Infinite sets that satisfy the principle of omniscience in
constructive type theory

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.

Tarmo Uustalu

Last update 26 May 2017