See [Localization in Homotopy Type theory](https://arxiv.org/abs/1807.04155)