Annotation: In this talk, we will discuss differences between homotopy and ordinary type theories. We will consider several constructions defined in HoTT (such as propositional truncation, quotient types, and the univalence axiom) and give some examples of their applications. In particular, we will consider a sorting function for lists of totally ordered elements, which shows that it is useful to define the disjunction as the join of types.
Speaker: Valery Isaev
23.09.2019, 17:15.
State University, Stary Peterhof, Universitetski pr., 28