Property-like structures in Homotopy Type Theory

The project seeks to explore the distinction between structure (such as that of a group) and a property (such as that of being Abelian) in the context of Homotopy Type Theory. 

This distinction is particularly important in category theory, where one has to consider 'property-like' structures, i.e. structures that are determined by a universal property up to unique isomorphism (such as pullbacks). 

The project aims to shed new light on the existing theory, developed in the context of 2-dimensional category theory, making use of the notion of a homotopy level of a type and of the Univalence Axiom, both originally introduced by Voevodsky.