Let \(T\) be a base type theory. We work in the type theory of spaces in \(T\).

• -Every topos is categorically fibrant.
• -Let \(i:\mathord {\textnormal {\textsf {Level}}}\).
  • -\(\mathcal {E}(i)\) is categorically fibrant.
  • -\((X:\mathcal {E}(i))\mapsto X\) is a left fibration.