{-# 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       #-}