    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Definitions for types of functions.
    ------------------------------------------------------------------------

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

    {-# OPTIONS --cubical-compatible --safe #-}

    module Function.Definitions where

    open import Data.Product.Base using (∃; _×_)
    open import Level using (Level)
    open import Relation.Binary.Core using (Rel)

    private
      variable
        a ℓ₁ ℓ₂ : Level
        A B : Set a

    ------------------------------------------------------------------------
    -- Basic definitions

    module _
      (_≈₁_ : Rel A ℓ₁) -- Equality over the domain
      (_≈₂_ : Rel B ℓ₂) -- Equality over the codomain
      where

      Congruent : (A → B) → Set _
      Congruent f = ∀ {x y} → x ≈₁ y → f x ≈₂ f y

      Injective : (A → B) → Set _
      Injective f = ∀ {x y} → f x ≈₂ f y → x ≈₁ y

      Surjective : (A → B) → Set _
      Surjective f = ∀ y → ∃ λ x → ∀ {z} → z ≈₁ x → f z ≈₂ y

      Bijective : (A → B) → Set _
      Bijective f = Injective f × Surjective f

      Inverseˡ : (A → B) → (B → A) → Set _
      Inverseˡ f g = ∀ {x y} → y ≈₁ g x → f y ≈₂ x

      Inverseʳ : (A → B) → (B → A) → Set _
      Inverseʳ f g = ∀ {x y} → y ≈₂ f x → g y ≈₁ x

      Inverseᵇ : (A → B) → (B → A) → Set _
      Inverseᵇ f g = Inverseˡ f g × Inverseʳ f g

    ------------------------------------------------------------------------
    -- Strict definitions

    -- These are often easier to use once but much harder to compose and
    -- reason about.

    StrictlySurjective : Rel B ℓ₂ → (A → B) → Set _
    StrictlySurjective _≈₂_ f = ∀ y → ∃ λ x → f x ≈₂ y

    StrictlyInverseˡ : Rel B ℓ₂ → (A → B) → (B → A) → Set _
    StrictlyInverseˡ _≈₂_ f g = ∀ y → f (g y) ≈₂ y

    StrictlyInverseʳ : Rel A ℓ₁ → (A → B) → (B → A) → Set _
    StrictlyInverseʳ _≈₁_ f g = ∀ x → g (f x) ≈₁ x