Gluing in Homotopy Type Theory - Michael Shulman