{-# OPTIONS --universe-polymorphism #-}

module MiniLibrary.Codata where



open import Level

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