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

Datum objave: 3. 5. 2022
Seminar za temelje matematike in teoretično računalništvo
četrtek
26
maj
Ura:
10.00 - 12.00
Lokacija:
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.