------------------------------------------------------------------------
-- The Agda standard library
--
-- Relationships between properties of functions
------------------------------------------------------------------------

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

module Function.Consequences where

open import Data.Product
open import Function.Definitions
open import Level
open import Relation.Binary
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
open import Relation.Nullary.Negation using (¬_)
open import Relation.Nullary.Negation.Core using (contraposition)

private
  variable
    a b ℓ₁ ℓ₂ : Level
    A : Set a
    B : Set b

module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) {f f⁻¹} where

  inverseˡ⇒surjective : Inverseˡ ≈₁ ≈₂ f f⁻¹ → Surjective ≈₁ ≈₂ f
  inverseˡ⇒surjective invˡ y = (f⁻¹ y , invˡ y)

  inverseʳ⇒surjective : Inverseʳ ≈₁ ≈₂ f f⁻¹ → Surjective ≈₂ ≈₁ f⁻¹
  inverseʳ⇒surjective invʳ y = (f y , invʳ y)

module _ (From : Setoid a ℓ₁) {≈₂ : Rel B ℓ₂} where

  open Setoid From using () renaming (Carrier to A; _≈_ to ≈₁)

  inverseʳ⇒injective : ∀ {f f⁻¹} → Congruent ≈₂ ≈₁ f⁻¹ →
                       Inverseʳ ≈₁ ≈₂ f f⁻¹ → Injective ≈₁ ≈₂ f
  inverseʳ⇒injective {f} {f⁻¹} cong₂ invʳ {x} {y} x≈y = begin
    x         ≈˘⟨ invʳ x ⟩
    f⁻¹ (f x) ≈⟨  cong₂ x≈y ⟩
    f⁻¹ (f y) ≈⟨  invʳ y ⟩
    y         ∎
    where open SetoidReasoning From

  inverseᵇ⇒bijective : ∀ {f f⁻¹} → Congruent ≈₂ ≈₁ f⁻¹ → Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Bijective ≈₁ ≈₂ f
  inverseᵇ⇒bijective cong₂ (invˡ , invʳ) =
    (inverseʳ⇒injective cong₂ invʳ , inverseˡ⇒surjective ≈₁ ≈₂ invˡ)

module _
  {f : A → B} (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂)
  where

  contraInjective : Injective _≈₁_ _≈₂_ f →
                    ∀ {x y} → ¬ (x ≈₁ y) → ¬ (f x ≈₂ f y)
  contraInjective inj p = contraposition inj p