.. todo:: heterogeneous Id types (used in e.g. cubicaltt)
The principle that there is only one type \Omega of propositions, and it is a member of \mathcal{U}_0: so all types of propositions \mathsf{Prop}_i are equal, and it is a type in the lowest universe.
Assuming this principle, the set of types of any universe is a topos.
Assuming this principle, some HITs become definable by impredicative encoding: e.g. truncation as \prod_{P:\Omega}(X\to P)\to P.
:ref:`UniMath <proof_assistants_libraries>` uses propositional resizing.
Induction-induction is different from induction-recursion.
See also Andrej Bauer on CS.StackExchange as well as :cite:`forsberg:setzer:indind`.
.. todo:: aka GADTs (?): every instance of a datatype declaration is
really just a W-type. compare with unimath (which doesn't
assume to have them). (well, this is not quite true: should
also consider the computation rules.)
.. todo:: - pi-types - altenkirch's presentation?