------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of functions, such as associativity and commutativity
------------------------------------------------------------------------

-- This file contains some core definitions which are reexported by
-- Algebra.FunctionProperties. They are placed here because
-- Algebra.FunctionProperties is a parameterised module, and some of
-- the parameters are irrelevant for these definitions.

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

module Algebra.FunctionProperties.Core where

open import Level

------------------------------------------------------------------------
-- Unary and binary operations

Op₁ :  {}  Set   Set 
Op₁ A = A  A

Op₂ :  {}  Set   Set 
Op₂ A = A  A  A