{-# OPTIONS --copatterns #-}
open import Common.Size

mutual
  data D (i : Size) : Set where
    c : ∀ (j : Size< i) → R j → D i

  record R (i : Size) : Set where
    coinductive
    constructor delay
    field       force : D i
open R

-- coinductive definition of inhabitant
mutual
  inR : R ∞
  force inR = inD

  inD : D ∞
  inD = c ∞ inR   -- ∞ < ∞

data ⊥ : Set where

-- inductive use of inhabitant
mutual
  loop : ∀ i → D i → ⊥
  loop i (c j r) = loopR j r

  loopR : ∀ i → R i → ⊥
  loopR i r = loop i (force r)

absurd : ⊥
absurd = loop ∞ inD