# Andrej Bauer: HoTT HITs

Date: 10. 4. 2017

Source: Mathematics and theoretical computing seminar

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.