Seminar talk on Mathematical Structures in Dependent Type Theory