Andrej Bauer: HoTT HITs
Datum objave: 10. 4. 2017
Seminar za temelje matematike in teoretično računalništvo
Torek, 11. 4. 2017, od 12h do 14h, Plemljev seminar, Jadranska 19
Abstract: I will review the concept of higher-inductive type (HIT) in homotopy type theory, and then present the ongoing work with Niels van der Weide in which the existence of a certain class of HITs is established as soon as three specific kinds of HITs exist. I may also show the audience a partial Coq formalization of the theory of HITs.