SizeUniv : SizeUniv is inconsistent

[ionathanch]

I guess this is fairly obvious since it's exactly the same as type-in-type but I thought I might as well create an explicit example since I didn't see one around (based on Hurkin's paradox). It also means sized types aren't consistent merely by removing ∞ < ∞. Wasn't SizeUniv formerly somewhere in the universe hierarchy?

-- Agda 2.6.2
{-# OPTIONS --sized-types #-}

open import Size
data False : SizeUniv where
data ⊥ : Set where

℘ : SizeUniv → SizeUniv
℘ S = S → SizeUniv

U : SizeUniv
U = ∀ (X : SizeUniv) → (℘ (℘ X) → X) → ℘ (℘ X)

τ : ℘ (℘ U) → U
τ t = λ X f p → t (λ x → p (f (x X f)))

σ : U → ℘ (℘ U)
σ s = s U τ

Δ : ℘ U
Δ y = (∀ p → σ y p → p (τ (σ y))) → False

Ω : U 
Ω = τ (λ p → (∀ x → σ x p → p x))

R : ∀ p → (∀ x → σ x p → p x) → p Ω
R _ 𝟙 = 𝟙 Ω (λ x → 𝟙 (τ (σ x)))

M : ∀ x → σ x Δ → Δ x
M _ 𝟚 𝟛 = 𝟛 Δ 𝟚 (λ p → 𝟛 (λ y → p (τ (σ y))))

L : (∀ p → (∀ x → σ x p → p x) → p Ω) → False
L 𝟘 = 𝟘 Δ M (λ p → 𝟘 (λ y → p (τ (σ y))))

false : ⊥
false = falsifier (L R)
  where
  falsifier : False → ⊥
  falsifier ()

[nad]

I think the idea is that SizeUniv should only contain Size and Size<: 628fdcf.

[nad]

More potentially problematic code:

primitive
  primLockUniv : Set₁

data D : primLockUniv where

However, the following code is rejected:

primitive
  primLockUniv : Set₁

_ : primLockUniv
_ = primLockUniv

The following code is also rejected:

{-# OPTIONS --cubical #-}

open import Agda.Primitive.Cubical

data D : IUniv where

[ionathanch]

I think the idea is that SizeUniv should only contain Size and Size<

How function types into types in SizeUniv are typed will have to change then, since SizeUniv is a little... impredicative? In any case, ⊥ doesn't need to be a data def:

{-# OPTIONS --sized-types #-}

imp : SizeUniv
imp = Set → Size

⊥ : SizeUniv
⊥ = (X : SizeUniv) → X

Although I thought the reason you can define a data def in SizeUniv was because it's a sort, I'm surprised IUniv doesn't work the same way.

[andreasabel]

⊥ : SizeUniv
⊥ = (X : SizeUniv) → X

@ionathanch : I can get Agda to loop by eliminating \bot to get an inhabitant of Size< i for any i (which is inconsistent with the model of sizes). But I couldn't exploit this to show absurdity...

[ionathanch]

I managed to do so using ∞ but only because it's the only closed size expression, not using the ∞ < ∞ property, although the principle is the same as for #3026:

{-# OPTIONS --sized-types #-}
open import Size

data ⊥ : Set where

postulate
  any : ∀ i → Size< i -- where we left off

data _<_ : Size → Size → Set where
  lt : ∀ s → (r : Size< s) → r < s

data Acc (s : Size) : Set where
  acc : (∀ {r} → r < s → Acc r) → Acc s

wf : ∀ s → Acc s
wf s = acc (λ {(lt .s r) → wf r})

¬wf : ∀ s → Acc s → ⊥
¬wf s (acc p) = ¬wf (any s) (p (lt s (any s)))

absurd : ⊥
absurd = (¬wf ∞) (wf ∞)

[andreasabel]

Here is the proof of inconsistency in its full glory:

-- AIM XXXV, 2022-05-06, issue #5891:
-- SizeUniv : SizeUniv was causing non-termination and inhabitation of Size< 0.
-- This is inconsistent; proof by Jonathan Chan.

{-# OPTIONS --sized-types #-}

open import Agda.Primitive
open import Agda.Builtin.Size

data ⊥ : Set where

-- Original exploit:
-- data False : SizeUniv where

False : SizeUniv
False = (X : SizeUniv) → X

-- Should fail.

-- Expected error:
-- Setω != SizeUniv
-- when checking that the expression (X : SizeUniv) → X has type SizeUniv

-- Step 1: Hurken's Paradox with SizeUniv : SizeUniv.

℘ : SizeUniv → SizeUniv
℘ S = S → SizeUniv

U : SizeUniv
U = ∀ (X : SizeUniv) → (℘ (℘ X) → X) → ℘ (℘ X)

τ : ℘ (℘ U) → U
τ t = λ X f p → t (λ x → p (f (x X f)))

σ : U → ℘ (℘ U)
σ s = s U τ

Δ : ℘ U
Δ y = (∀ p → σ y p → p (τ (σ y))) → False

Ω : U
Ω = τ (λ p → (∀ x → σ x p → p x))

R : ∀ p → (∀ x → σ x p → p x) → p Ω
R _ 𝟙 = 𝟙 Ω (λ x → 𝟙 (τ (σ x)))

M : ∀ x → σ x Δ → Δ x
M _ 𝟚 𝟛 = 𝟛 Δ 𝟚 (λ p → 𝟛 (λ y → p (τ (σ y))))

L : (∀ p → (∀ x → σ x p → p x) → p Ω) → False
L 𝟘 = 𝟘 Δ M (λ p → 𝟘 (λ y → p (τ (σ y))))

-- Prevent unfolding, as this term has no whnf.
-- Stops Agda from looping.

abstract
  false : False
  false = L R

-- This gives us a predecessor on Size.

size-pred : ∀ i → Size< i
size-pred i = false (Size< i)

-- Step 2: Size predecessor is inconsistent.

-- Jonathan Chan:
-- I managed to do so using ∞ but only because it's the only closed
-- size expression, not using the ∞ < ∞ property, although the
-- principle is the same as for #3026:

data _>_ (s : Size) : Size → Set where
  lt : (r : Size< s) → s > r

data Acc (s : Size) : Set where
  acc : (∀ {r} → s > r → Acc r) → Acc s

wf : ∀ s → Acc s
wf s = acc λ{ (lt r) → wf r }

¬wf : ∀ s → Acc s → ⊥
¬wf s (acc p) = ¬wf (size-pred s) (p (lt (size-pred s)))

absurd : ⊥
absurd = (¬wf ∞) (wf ∞)