2
$\begingroup$

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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
3
$\begingroup$

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.

Improve this answer
$\endgroup$
4
  • $\begingroup$ Is this 'just' a failure of normalization in 'false' contexts? That's an annoying property for a theory to have, but it isn't always a deal breaker. For instance, extensional type theory has this problem, I think, but it isn't usually considered "not computational." $\endgroup$
    – Dan Doel
    Feb 7, 2023 at 17:19
  • $\begingroup$ I know of people who would challenge the claim that extensional TT is computational, exactly for this reason: you cannot easily reduce under a context, because all kinds of good computational properties (typically, subject reduction) are lost (and the context need not even be inconsistent for this, it suffices to break injectivity of product types). As far as I know, and for this reason, for such type theories you can really only assign a computational behaviour to derivations rather than just terms. $\endgroup$
    – Meven Lennon-Bertrand
    Feb 8, 2023 at 9:51
  • $\begingroup$ @MevenLennon-Bertrand: wouldn't subject reduction still hold, provided one has fully annotated terms? (Extensional type theory without fully annotated terms is deeply broken in more than one way.) $\endgroup$
    – Andrej Bauer
    Feb 8, 2023 at 14:08
  • $\begingroup$ If you do that, I guess that before firing a β-redex you would then need to decide whether it is safe, by comparing annotations (in which case I believe you'd get SR back). But this makes your "computational content" depend on typing information, which if you believe in realizability and untyped computation sounds somewhat dubious. But then again dynamic typing is a thing, and its runtime semantic does something similar to this, so… $\endgroup$
    – Meven Lennon-Bertrand
    Feb 8, 2023 at 18:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.