------------------------------------------------------------------------
-- The Agda standard library
--
-- Core definitions for Functions
------------------------------------------------------------------------

-- The contents of this file should usually be accessed from `Function`.

{-# OPTIONS --without-K --safe #-}

module Function.Core where

------------------------------------------------------------------------
-- Types

Fun₁ :  {a}  Set a  Set a
Fun₁ A = A  A

Fun₂ :  {a}  Set a  Set a
Fun₂ A = A  A  A