Home > News > Andrej Bauer: HoTT HITs

Andrej Bauer: HoTT HITs

Date: 10. 4. 2017
Source: Mathematics and theoretical computing seminar
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.