Previous Special Year Seminar

Isomorphic Structures of any Kind are `Equal' in HoTT: But What is a Kind of Structure?

A Quillen Model Structure in Type Theory

The Calculus of Opetopes

Weak Infinity Groupoids in HoTT