⚠️ Archived site. This is the pre-3.0 Agda Universal Algebra Library, preserved for reference. Its current home is agda-algebras.universalalgebra.org (as of July 2026).
------------------------------------------------------------------------ -- The Agda standard library -- -- Core definitions for Functions ------------------------------------------------------------------------ -- The contents of this file should always be accessed from `Function`. {-# OPTIONS --cubical-compatible --safe #-} module Function.Core where open import Level using (_⊔_) ------------------------------------------------------------------------ -- Types Fun₁ : ∀ {a} → Set a → Set a Fun₁ A = A → A Fun₂ : ∀ {a} → Set a → Set a Fun₂ A = A → A → A ------------------------------------------------------------------------ -- Morphism Morphism : ∀ {a} → ∀ {b} → Set a → Set b → Set (a ⊔ b) Morphism A B = A → B