    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Relationships between properties of functions where the equality
    -- over both the domain and codomain is assumed to be _≡_
    ------------------------------------------------------------------------

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

    module Function.Consequences.Propositional
      {a b} {A : Set a} {B : Set b}
      where

    open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; cong)
    open import Relation.Binary.PropositionalEquality.Properties
      using (setoid)
    open import Function.Definitions
      using (StrictlySurjective; StrictlyInverseˡ; StrictlyInverseʳ; Inverseˡ
            ; Inverseʳ; Surjective)
    open import Relation.Nullary.Negation.Core using (contraposition)

    import Function.Consequences.Setoid (setoid A) (setoid B) as Setoid

    ------------------------------------------------------------------------
    -- Re-export setoid properties

    open Setoid public
      hiding
      ( strictlySurjective⇒surjective
      ; strictlyInverseˡ⇒inverseˡ
      ; strictlyInverseʳ⇒inverseʳ
      )

    ------------------------------------------------------------------------
    -- Properties that rely on congruence

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

    strictlySurjective⇒surjective : StrictlySurjective _≡_ f →
                                     Surjective _≡_ _≡_ f
    strictlySurjective⇒surjective =
     Setoid.strictlySurjective⇒surjective (cong _)

    strictlyInverseˡ⇒inverseˡ : ∀ f → StrictlyInverseˡ _≡_ f f⁻¹ →
                                Inverseˡ _≡_ _≡_ f f⁻¹
    strictlyInverseˡ⇒inverseˡ f =
      Setoid.strictlyInverseˡ⇒inverseˡ (cong _)

    strictlyInverseʳ⇒inverseʳ : ∀ f → StrictlyInverseʳ _≡_ f f⁻¹ →
                                Inverseʳ _≡_ _≡_ f f⁻¹
    strictlyInverseʳ⇒inverseʳ f =
      Setoid.strictlyInverseʳ⇒inverseʳ (cong _)