------------------------------------------------------------------------ -- 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 the -- parameters are irrelevant for these definitions. module Algebra.FunctionProperties.Core where ------------------------------------------------------------------------ -- Unary and binary operations Op₁ : Set → Set Op₁ A = A → A Op₂ : Set → Set Op₂ A = A → A → A