# Naive computation of propositional resizing

As far as I know, it is not known whether cubical type theories with propositional resizing admit computational interpretations. But here is an obvious attempt: Turn off universe checking locally, and simply define $$r : \mathsf{hProp}_i \to \mathsf{hProp}_0$$ to be the identity function (or perhaps wrapped in a trivial inductive type, etc). For example in Agda:

{-# NO_UNIVERSE_CHECK #-}
record Resize {i} (p : Type i) (q : isProp p) : Type where
constructor wrap
field
get : p


What could go wrong?

I realized the answer very quickly. It goes wrong immediately. In a context with O : {i : Level}(p : Type i) -> isProp p, we can formulate Russell's paradox with no difficulty. But since Resize doesn't inspect the proof of propositionality at all, the computation does not get stuck on the variable O, and it loops forever, just like the regular Russell's paradox in Agda.