    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Relationships between properties of functions where the equality
    -- over both the domain and codomain are assumed to be setoids.
    ------------------------------------------------------------------------

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

    open import Relation.Binary.Bundles using (Setoid)

    module Function.Consequences.Setoid
      {a b ℓ₁ ℓ₂}
      (S : Setoid a ℓ₁)
      (T : Setoid b ℓ₂)
      where

    open import Function.Definitions
    open import Relation.Nullary.Negation.Core using (¬_)

    import Function.Consequences as C

    private
      open module S = Setoid S using () renaming (Carrier to A; _≈_ to ≈₁)
      open module T = Setoid T using () renaming (Carrier to B; _≈_ to ≈₂)

      variable
        f : A → B
        f⁻¹ : B → A

    ------------------------------------------------------------------------
    -- Injective

    contraInjective : Injective ≈₁ ≈₂ f →
                      ∀ {x y} → ¬ (≈₁ x y) → ¬ (≈₂ (f x) (f y))
    contraInjective = C.contraInjective ≈₂

    ------------------------------------------------------------------------
    -- Inverseˡ

    inverseˡ⇒surjective : Inverseˡ ≈₁ ≈₂ f f⁻¹ → Surjective ≈₁ ≈₂ f
    inverseˡ⇒surjective = C.inverseˡ⇒surjective ≈₂

    ------------------------------------------------------------------------
    -- Inverseʳ

    inverseʳ⇒injective : ∀ f → Inverseʳ ≈₁ ≈₂ f f⁻¹ → Injective ≈₁ ≈₂ f
    inverseʳ⇒injective f = C.inverseʳ⇒injective ≈₂ f T.refl S.sym S.trans

    ------------------------------------------------------------------------
    -- Inverseᵇ

    inverseᵇ⇒bijective : Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Bijective ≈₁ ≈₂ f
    inverseᵇ⇒bijective = C.inverseᵇ⇒bijective ≈₂ T.refl S.sym S.trans

    ------------------------------------------------------------------------
    -- StrictlySurjective

    surjective⇒strictlySurjective : Surjective ≈₁ ≈₂ f →
                                     StrictlySurjective ≈₂ f
    surjective⇒strictlySurjective =
      C.surjective⇒strictlySurjective ≈₂ S.refl

    strictlySurjective⇒surjective : Congruent ≈₁ ≈₂ f →
                                     StrictlySurjective ≈₂ f →
                                     Surjective ≈₁ ≈₂ f
    strictlySurjective⇒surjective =
      C.strictlySurjective⇒surjective T.trans

    ------------------------------------------------------------------------
    -- StrictlyInverseˡ

    inverseˡ⇒strictlyInverseˡ : Inverseˡ ≈₁ ≈₂ f f⁻¹ →
                                StrictlyInverseˡ ≈₂ f f⁻¹
    inverseˡ⇒strictlyInverseˡ = C.inverseˡ⇒strictlyInverseˡ ≈₁ ≈₂ S.refl

    strictlyInverseˡ⇒inverseˡ : Congruent ≈₁ ≈₂ f →
                                StrictlyInverseˡ ≈₂ f f⁻¹ →
                                Inverseˡ ≈₁ ≈₂ f f⁻¹
    strictlyInverseˡ⇒inverseˡ = C.strictlyInverseˡ⇒inverseˡ T.trans

    ------------------------------------------------------------------------
    -- StrictlyInverseʳ

    inverseʳ⇒strictlyInverseʳ : Inverseʳ ≈₁ ≈₂ f f⁻¹ →
                                StrictlyInverseʳ ≈₁ f f⁻¹
    inverseʳ⇒strictlyInverseʳ = C.inverseʳ⇒strictlyInverseʳ ≈₁ ≈₂ T.refl

    strictlyInverseʳ⇒inverseʳ : Congruent ≈₂ ≈₁ f⁻¹ →
                                StrictlyInverseʳ ≈₁ f f⁻¹ →
                                Inverseʳ ≈₁ ≈₂ f f⁻¹
    strictlyInverseʳ⇒inverseʳ = C.strictlyInverseʳ⇒inverseʳ S.trans