Paper: https://arxiv.org/abs/1701.05617 (actually this is a formalization of an unpublished newer version)
This code uses Agda's instance arguments to clarify which theorems rely on certain type-theoretical axioms such as function extensionality or univalence.
To support these, use the ua-instance branch of abooij/HoTT-Agda.