The axiom of univalence was originally justified by Voevodsky’s simplical set model. This model is however not constructive and (Bezem, Coquand and Huber 2014 [2013]) has more recently proposed a model in Kan cubical sets.