Working with Mathematical Structures in Type Theory