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

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

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

open import Relation.Binary

module Function.Definitions
  {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
  (_≈₁_ : Rel A ℓ₁) -- Equality over the domain
  (_≈₂_ : Rel B ℓ₂) -- Equality over the codomain
  where

open import Data.Product using (; _×_)
import Function.Definitions.Core1 as Core₁
import Function.Definitions.Core2 as Core₂
open import Function.Base
open import Level using (_⊔_)

------------------------------------------------------------------------
-- Definitions

Congruent : (A  B)  Set (a  ℓ₁  ℓ₂)
Congruent f =  {x y}  x ≈₁ y   f x ≈₂ f y

Injective : (A  B)  Set (a  ℓ₁  ℓ₂)
Injective f =  {x y}  f x ≈₂ f y  x ≈₁ y

open Core₂ {A = A} _≈₂_ public
  using (Surjective)

Bijective : (A  B)  Set (a  b  ℓ₁  ℓ₂)
Bijective f = Injective f × Surjective f

open Core₂ {A = A} _≈₂_ public
  using (Inverseˡ)

open Core₁ {B = B} _≈₁_ public
  using (Inverseʳ)

Inverseᵇ : (A  B)  (B  A)  Set (a  b  ℓ₁  ℓ₂)
Inverseᵇ f g = Inverseˡ f g × Inverseʳ f g