Equality is incompatible with sized types

[andreasabel]

open import Size
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.PropositionalEquality.TrustMe

data ⊥ : Set where

data SizeLt (i : Size) : Set where
  [_] : (j : Size< i) → SizeLt i

module OneSize where 

  eq! : ∀ (i j : Size) → i ≡ j
  eq! _ _ = trustMe

  cast : ∀ i j → SizeLt i → SizeLt j
  cast i j = subst SizeLt (eq! i j)

  foo : ∀ i → SizeLt i → ⊥
  foo i [ j ] = foo j (cast i j [ j ])

  test : ⊥
  test = foo ∞ [ ∞ ]

The term test is looping.

[Saizan]

Without using trustMe, but proofs of equality to \infty instead.

open import Size
open import Relation.Binary.PropositionalEquality

data ⊥ : Set where

data SizeLt (i : Size) : Set where
  [_] : (j : Size< i) → SizeLt i

get : ∀ {i} → SizeLt i → Size
get [ j ] = j

module OneSize where

  eq! : ∀ (i j : Size) → i ≡ ∞ → j ≡ ∞ → i ≡ j
  eq! _ _ refl refl = refl

  cast : ∀ i j → i ≡ ∞ → j ≡ ∞ → SizeLt i → SizeLt j
  cast i j i∞ j∞ = subst SizeLt (eq! i j i∞ j∞)

  cast-∞ : ∀ i (j : SizeLt i)
           (i∞ : i ≡ ∞) (j∞ : get j ≡ ∞) →
            get (cast i (get j) i∞ j∞ j) ≡ ∞
  cast-∞ _ [ _ ] refl refl = refl

  foo : ∀ i → (j : SizeLt i) → i ≡ ∞ → get j ≡ ∞ → ⊥
  foo i [ j ] i∞ j∞ = foo j
                          (cast i j i∞ j∞ [ j ])
                          j∞
                          (cast-∞ i [ j ] i∞ j∞)

  test : ⊥
  test = foo ∞ [ ∞ ] refl refl

[andreasabel]

And the slightly dubious get function... Is this related to #1428?

[Saizan]

Isn't ∞ : Size< ∞ the most dubious part here? :)

[Saizan]

Without using the get function:

open import Size
open import Relation.Binary.PropositionalEquality

data ⊥ : Set where

data SizeLt∞ (i : Size) : Set where
  [_,_] : (j : Size< i) → j ≡ ∞ → SizeLt∞ i

module OneSize where

  cast : ∀ i j → i ≡ ∞ → j ≡ ∞ → SizeLt∞ i → SizeLt∞ j
  cast i j refl refl [ k , eq ] = [ k , eq ]

  foo : ∀ i → (j : SizeLt∞ i) → i ≡ ∞ → ⊥
  foo i [ j , j∞ ] i∞ = foo j (cast i j i∞ j∞ [ j , j∞ ]) j∞

  test : ⊥
  test = foo ∞ [ ∞ , refl ] refl

[UlfNorell]

Time to bring back the size universe?

[andreasabel]

The trouble with SizeUniv was that since the introduction of universe polymorphism much of the sort machinery relies on the fact that we have a linear hierarchy of sorts. This needs to be refactored properly to accommodate other PTSs than {Set i | i in Nat}.

[UlfNorell]

Without standard library

open import Agda.Builtin.Size renaming (ω to ∞)
open import Agda.Builtin.Equality

data ⊥ : Set where

data SizeLt∞ (i : Size) : Set where
  [_,_] : (j : Size< i) → j ≡ ∞ → SizeLt∞ i

cast : ∀ i j → i ≡ ∞ → j ≡ ∞ → SizeLt∞ i → SizeLt∞ j
cast i j refl refl [ k , eq ] = [ k , eq ]

foo : ∀ i → (j : SizeLt∞ i) → i ≡ ∞ → ⊥
foo i [ j , j∞ ] i∞ = foo j (cast i j i∞ j∞ [ j , j∞ ]) j∞

test : ⊥
test = foo ∞ [ ∞ , refl ] refl

[nad]

And the slightly dubious get function...

Is the following code not supposed to work?

------------------------------------------------------------------------
-- Size elimination

-- A trick is used to implement size elimination. This trick was
-- suggested to me by Andrea Vezzosi.

-- A data type wrapping Size<_.
--
-- If this wrapper is removed from the definition of elim below, then
-- that definition is rejected.

data [Size<_] (i : Size) : Set where
  box : Size< i → [Size< i ]

-- A projection.

unbox : ∀ {i} → [Size< i ] → Size< i
unbox (box j) = j

-- Size elimination.

elim :
  ∀ {p}
  (P : Size → Set p) →
  (∀ i → ((j : [Size< i ]) → P (unbox j)) → P i) →
  ∀ i → P i
elim P f i = f i λ { (box j) → elim P f j }

[nad]

The fact that ∞ : Size< ∞ seems to be problematic. Is this a fundamental problem, or can the problem be contained by, say, letting sizes live in a separate universe (so that we cannot talk about equality of sizes, for instance)?

[Saizan]

Avoiding equality of sizes does not seem to be enough, though if we would only allow irrelevant size quantification in datatypes it might.
(Personally I'd rather get rid of ∞ : Size< ∞ ! But it's not like I have a design ready either)

open import Agda.Builtin.Size renaming (ω to ∞)
open import Agda.Builtin.Equality

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst                                                                                                                    

data ⊥ : Set where

data Nat (i : Size) : Set where
  zero : ∀ (j : Size< i) → Nat i
  suc : ∀ (j : Size< i) → Nat j → Nat i

data SizeLt (i : Size) : Set where
  [_] : (j : Size< i) → SizeLt i

SizeLt∞ : (i : Size) → Set
SizeLt∞ i = Σ (SizeLt i) \ { [ j ] → zero j ≡ zero ∞ }

Type : Size → Nat ∞ → Set
Type i (zero j) = SizeLt∞ i → SizeLt∞ j
Type i (suc j _) = SizeLt∞ i → SizeLt∞ j

cast : ∀ i (n : Nat ∞) → n ≡ zero ∞ → Type i n
cast i .(zero ∞) refl ([ k ] , eq) = [ k ] , eq

foo : ∀ i → (j : SizeLt∞ i) → ⊥
foo i ([ j ] , j∞) = foo j (cast i (zero j) j∞ ([ j ] , j∞))

test : ⊥
test = foo ∞ ([ ∞ ] , refl)