 Crosilla and Rathjen’s set theory with inaccessible sets (but no set induction) is proof theoretically rather weak, but mathematically quite expressive. For example, it has been used to verify that the addition of Voevodsky’s Univalence Axiom to Martin-Löf type theory does not engender impredicativity (Rathjen 2017). The axiom of Univalence was introduced by Voevodsky as part of his Univalent Foundations programme (Voevodsky 2015). (For Univalent Foundations, see the entries on   type theory  and on  intuitionistic type theory).  Voevodsky gave a model of constructive type theory with the Univalence Axiom which is based on Kan simplicial sets (see Kapulkin &amp; Lumsdaine 2012, Other Internet Resources). The simplicial model of constructive type theory with univalence developed in the above article is carried out within an extension of ZFC with inaccessible cardinals. This prompted the question whether one could give a more constructive model of this type theory, and, in particular, whether the type theory is predicative. Bezem, Coquand and Huber (2014) have recently proposed a model of this type theory in cubical sets which is computational and “can be expressed in a constructive metalogic”. Rathjen (2017) has verified that this new model can be codified in a suitable extension of CZF by inaccessible sets which is much weaker than classical set theory with inaccessible cardinals. In fact, it turns out that if we take as starting point a relatively weak type theory, i.e. one without W-types, and extend it by the Univalence Axiom, the resulting theory has proof theoretic strength \(\Gamma_0\), the ordinal usually taken to represent the limit of predicativity given the natural numbers (Rathjen 2017). To show this, one proves that the cubical model by Bezem, Coquand and Huber can be carried out in an extension of the system introduced in Crosilla and Rathjen (2001) by (bounded) Relativized Dependent Choice. It follows from (Crosilla and Rathjen 2001) and (Rathjen 2003) that the latter has proof theoretic ordinal \(\Gamma_0\). 