------------------------------------------------------------------------
-- The Agda standard library
--
-- Definitions for types of functions that only require an equality
-- relation over the co-domain.
------------------------------------------------------------------------

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

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

open import Relation.Binary

module Function.Definitions.Core2
  {b ℓ₂} {B : Set b} (_≈₂_ : Rel B ℓ₂)
  where

open import Data.Product using ()
open import Level using (Level; _⊔_)

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

Surjective :  {a} {A : Set a}  (A  B)  Set (a  b  ℓ₂)
Surjective f =  y   λ x  f x ≈₂ y

-- (Note the name `LeftInverse` is used for the bundle)
Inverseˡ :  {a} {A : Set a}  (A  B)  (B  A)  Set (b  ℓ₂)
Inverseˡ f g =  x  f (g x) ≈₂ x