Martín Escardó: Searchable types in HoTT/UF

I will show how to define plenty of infinite exhaustibly searchable types in HoTT/UF. We'll measure the logical complexity of the searchable types using ordinals. In particular, I'll define a universe à la Tarski of searchable ordinals by induction-recursion. This has been coded in Agda.