# Pastebin IAa8kCTr
record M {i : Size} {ℓ} (A : Set ℓ) (B : A → Set ℓ) : Set ℓ where
  constructor cosup
  coinductive
  field
    head : A
    tail : {j : Size< i} → B head → M {j} A B
open M public