    {-# OPTIONS --cubical-compatible --safe --universe-polymorphism --no-sized-types
                --guardedness --level-universe #-}

    module Agda.Builtin.Coinduction where

    infix 1000 ♯_

    postulate
      ∞  : ∀ {a} (A : Set a) → Set a
      ♯_ : ∀ {a} {A : Set a} → A → ∞ A
      ♭  : ∀ {a} {A : Set a} → ∞ A → A

    {-# BUILTIN INFINITY ∞  #-}
    {-# BUILTIN SHARP    ♯_ #-}
    {-# BUILTIN FLAT     ♭  #-}