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

{-# OPTIONS --without-K --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 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