proof that, for any function, existence of a left inverse ⇔ injectivity

injectivity.agda

open import Function using (Func)
open import Relation.Binary using (Setoid)
open import Relation.Nullary using (Dec; yes; no)
open import Data.Product using (_,_; ∃-syntax)
open import Level using (_⊔_)
import Relation.Binary.Reasoning.Setoid as Reasoning
open Setoid using (sym; refl)
open Func using (cong)

module injectivity
  {a b ℓ₁ ℓ₂} {A : Setoid a ℓ₁} {B : Setoid b ℓ₂}
  where

open Setoid A renaming (_≈_ to _≈₁_)
open Setoid B renaming (_≈_ to _≈₂_)

private
  Lem = ∀ {ℓ} (P : Set ℓ) → Dec P

-- statements

IsInverse : Func A B → Func B A → Set (a ⊔ ℓ₁)
IsInverse f' g' = ∀ x → g (f x) ≈₁ x
  where open Func f' using (f); open Func g' renaming (f to g)

Invertible : Func A B → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
Invertible f = ∃[ g ] IsInverse f g

Injective : Func A B → Set (a ⊔ ℓ₁ ⊔ ℓ₂)
Injective f' = ∀ x₁ x₂ → f x₁ ≈₂ f x₂ → x₁ ≈₁ x₂
  where open Func f' using (f)

-- proof in both directions

invertible⇒injective : ∀ (f : Func A B) → Invertible f → Injective f
invertible⇒injective f' (g' , inv) x₁ x₂ y₁≈y₂ = begin
  x₁       ≈⟨ sym A (inv x₁) ⟩
  g (f x₁) ≈⟨ cong g' y₁≈y₂ ⟩
  g (f x₂) ≈⟨ inv x₂ ⟩
  x₂       ∎
  where open Func f' using (f); open Func g' renaming (f to g); open Reasoning A

injective⇒invertible : Lem → ∀ (f : Func A B) → (Func B A) → Injective f → Invertible f
injective⇒invertible lem f' g' inj = inverse , proof
  where
  open Func f' using (f); open Func g' renaming (f to g)

  inverse : Func B A

  inverse .Func.f y with lem (∃[ x ] f x ≈₂ y)
  ...          | yes (x , _) = x
  ...          | no  _       = g y

  proof : IsInverse f' inverse
  proof x₀ with lem (∃[ x ] f x ≈₂ f x₀)
  ...         | yes (x , p) = inj x x₀ p
  ...         | no  ¬p with () ← ¬p (x₀ , refl B)