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

open import Function.Definitions
open import Level
open import Relation.Nullary.Negation.Core using (contraposition)
open import Relation.Binary.PropositionalEquality.Core
  using (_≡_; _≢_; refl; sym; trans; cong)

import Function.Consequences as C

private
  variable
    a b ℓ₁ ℓ₂ : Level
    A B : Set a
    f f⁻¹ : A → B

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

contraInjective : Injective _≡_ _≡_ f →
                  ∀ {x y} → x ≢ y → f x ≢ f y
contraInjective inj p = contraposition inj p

------------------------------------------------------------------------
-- 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 refl sym trans

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

inverseᵇ⇒bijective : Inverseᵇ _≡_ _≡_ f f⁻¹ → Bijective _≡_ _≡_ f
inverseᵇ⇒bijective = C.inverseᵇ⇒bijective _≡_ refl sym trans

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

surjective⇒strictlySurjective : Surjective _≡_ _≡_ f →
                                 StrictlySurjective _≡_ f
surjective⇒strictlySurjective =
  C.surjective⇒strictlySurjective _≡_ refl

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

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

inverseˡ⇒strictlyInverseˡ : Inverseˡ _≡_ _≡_ f f⁻¹ →
                            StrictlyInverseˡ _≡_ f f⁻¹
inverseˡ⇒strictlyInverseˡ =
  C.inverseˡ⇒strictlyInverseˡ _≡_ _≡_ refl

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

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

inverseʳ⇒strictlyInverseʳ : Inverseʳ _≡_ _≡_ f f⁻¹ →
                            StrictlyInverseʳ _≡_ f f⁻¹
inverseʳ⇒strictlyInverseʳ = C.inverseʳ⇒strictlyInverseʳ _≡_ _≡_ refl

strictlyInverseʳ⇒inverseʳ : ∀ f →
                            StrictlyInverseʳ _≡_ f f⁻¹ →
                            Inverseʳ _≡_ _≡_ f f⁻¹
strictlyInverseʳ⇒inverseʳ {f⁻¹ = f⁻¹} _ =
  C.strictlyInverseʳ⇒inverseʳ trans (cong f⁻¹)