Martín Escardó: Searchable types in HoTT/UF
Date of publication: 3. 5. 2022
Mathematics and theoretical computing seminar
Thursday
26
May
Time:
10:00 - 12:00
Location:
3.07
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.
