------------------------------------------------------------------------
-- 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