A formal treatment of univalent completions

Date:

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

The extended abstract can be found here.