Gluing in Homotopy Type Theory