A Library of Monoidal Categories for Display and Univalence

Date:

A workshop talk presented (online) at the Workshop on Homotopy Type Theory/Univalent Foundations.

The extended abstract can be found here.