Made some progress on proposal, amongst other small details.
Some experimentation with Agda and basic HoTT results regarding n-truncations.