The code in decomposing-ua formalises the arguments made in the earlier sections of the paper about decomposing the univalence axiom into other axioms. The main entry point is Decomp.agda.
The code in cubical-topos-decomp formalises the constructions performed in the internal language of the cubical sets topos in order to verify the new axioms. The main entry point is root.agda.
This development successfully typechecks with Agda 2.5.4.