```{- With Agda's current sized types, we have a size ∞ with ∞ < ∞. That's
obviously troublesome if we want to interpret sizes as ordinals and < as the
less-than relation, and indeed we can use this rule to prove false (in
multiple different ways).

This file is an experiment to see whether we could still work with a system
that doesn't have this rule.
-}

{-# OPTIONS --postfix-projections #-}
module irreflexive-lt where

open import Size

postulate
𝟘 : Size

data Size≲ : (j : Size) → Set where
≲∞ : (i : Size) → Size≲ ∞
<→≲ : ∀ {j} (i : Size< j) → Size≲ j

from≲ : ∀ {j} → Size≲ j → Size
from≲ (≲∞ i) = i
from≲ (<→≲ i) = i

∞′ : Size≲ ∞
∞′ = ≲∞ ∞

--------------------------------------------------------------------------------
-- Natural numbers

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

-- Using the successor at size ∞ becomes nontrivial. The following is NOT
-- allowed since we use (∞ : Size< ∞).
-- suc₀ : ℕ ∞ → ℕ ∞
-- suc₀ n = suc ∞ n

-- Workaround: superfluous pattern matching.
suc₁ : ℕ ∞ → ℕ ∞
suc₁ zero = suc 𝟘 zero
suc₁ (suc j x) = suc (↑ j) (suc j x)

-- Case analysis
caseℕ : {T : Set} → (i : Size) → ℕ i → T → ((j : Size< i) → ℕ j → T) → T
caseℕ i zero z s = z
caseℕ i (suc j n) z s = s j n

-- Dependent elimination (with size-based termination).
indℕ : (P : (i : Size) → ℕ i → Set)
→ ((i : Size) → P i zero)
→ ((i : Size) (j : Size< i) (n : ℕ j) → P j n → P i (suc j n))
→ (i : Size) (n : ℕ i) → P i n
indℕ P Z S i zero = Z i
indℕ P Z S i (suc j n) = S i j n (indℕ P Z S j n)

--------------------------------------------------------------------------------
-- Streams

record 𝕊 (A : Set) (i : Size) : Set where
coinductive
field
tail : (j : Size< i) → 𝕊 A j

open 𝕊

variable
A B : Set

-- Again, we CANNOT use tail at ∞ directly since this uses (∞ : Size< ∞).
-- tail₀ : 𝕊 ∞ → 𝕊 ∞
-- tail₀ xs = tail xs ∞

-- Workaround: The equivalent of the 'superfluous pattern matching' workaround
-- for suc.
tail₁ : 𝕊 A ∞ → 𝕊 A ∞
tail₁ xs .head = head {i = 𝟘} (tail xs 𝟘) -- [1]
tail₁ xs .tail j = tail (tail xs (↑ j)) j

-- [1] Without the implicit argument, this doesn't typecheck. Apparently the
-- size argument to head gets eagerly instantiated to ∞ or something.

replicate : (i : Size) → A → 𝕊 A i
replicate i a .head = a
replicate i a .tail j = replicate j a

map𝕊 : (A → B) → (i : Size) → 𝕊 A i → 𝕊 B i
map𝕊 f i xs .tail j = map𝕊 f j (tail xs j)

--------------------------------------------------------------------------------
-- Rose trees

data List (A : Set) : Set where
[] : List A
_∷_ : A → List A → List A

mapList : (A → B) → List A → List B
mapList f [] = []
mapList f (x ∷ xs) = f x ∷ mapList f xs

data Tree (A : Set) (i : Size) : Set where
leaf : A → Tree A i
node : (j : Size< i) → List (Tree A j) → Tree A i

mapTree : (A → B) → (i : Size) → Tree A i → Tree B i
mapTree f i (leaf x) = leaf (f x)
mapTree f i (node j cs) = node j (mapList (mapTree f j) cs)

--------------------------------------------------------------------------------
-- Potentially infinite lists

mutual
data CoList (A : Set) (i : Size) : Set where
[] : CoList A i
_∷_ : A → CoList′ A i → CoList A i

record CoList′ (A : Set) (i : Size) : Set where
coinductive
field
force : (j : Size< i) → CoList A j

open CoList′

open import Data.Product using (∃-syntax)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; inspect ; [_])
open import Relation.Binary.HeterogeneousEquality using (_≅_ ; refl)

postulate
force-parametric : ∀ {A i} (xs : CoList′ A i) (j j′ : Size< i)
→ xs .force j ≅ xs .force j′

size-parametric : ∀ {T : Size< ∞ → Set} (f : (i : Size< ∞) → T i)
→ (j j′ : Size< ∞)
→ f j ≅ f j′

mutual
data _≈_ {A i j} : CoList A i → CoList A j → Set where
[] : [] ≈ []
_∷_ : ∀ {x y xs ys}
→ x ≡ y
→ xs ≈′ ys
→ (x ∷ xs) ≈ (y ∷ ys)

record _≈′_ {A i j} (xs : CoList′ A i) (ys : CoList′ A j) : Set where
coinductive
field
force : (k : Size< i) (l : Size< j) → xs .force k ≈ ys .force l

open _≈′_

force∞ : CoList′ A ∞ → CoList A ∞
force∞ {A} xs with xs .force 𝟘
... | [] = []
... | y ∷ ys = y ∷ ys′
where
ys′ : CoList′ A ∞
ys′ .force i with xs .force (↑ i)
... | [] = []
... | z ∷ zs = zs .force i

𝕊→CoList : (i : Size) → 𝕊 A i → CoList A i
𝕊→CoList i xs = head xs ∷ λ { .force j → 𝕊→CoList j (tail xs j) }

-- Radical thought: Just kill ∞ altogether and work with (∀ i → CoList A i) and
-- (∃ i → List A i) directly. How much less useful does that make the system?
--
-- Perhaps we can auto-derive the iso (∃ i → List A i) ≅ List A.

-- Radical thought: What if we only provide the Thunk type from the stdlib? Can
-- we recover all other coinductive types from that?
```