Legacy.Base.Functions.Inverses

Inverses

This is the Legacy.Base.Functions.Inverses module of the agda-algebras library.

{-# OPTIONS --without-K --exact-split --safe #-}
module Legacy.Base.Functions.Inverses where

-- Imports from Agda and the Agda Standard Library ---------------------------------------------
open import Agda.Primitive    using () renaming ( Set to Type )
open import Data.Product      using ( _,_ ; Σ-syntax )
open import Level             using ( Level ; _⊔_ )
open import Relation.Binary.PropositionalEquality
                              using ( _≡_ ; sym ; refl )
open import Relation.Unary    using ( Pred ; _∈_ )

-- Imports from agda-algebras ----------------------------------------------------------------
open import Overture.Basic using ( ∃-syntax ; ∣_∣ )

private variable a b : Level

We begin by defining an data type that represents the semantic concept of inverse image of a function.

module _ {A : Type a}{B : Type b} where

 data Image_∋_ (f : A → B) : B → Type (a ⊔ b) where
  eq : {b : B} → (a : A) → b ≡ f a → Image f ∋ b

 {-# WARNING_ON_USAGE Image_∋_ "Use Overture.Functions.Image_∋_ instead. Deprecated under #303; removal planned one minor cycle after #303 lands." #-}
 {-# WARNING_ON_USAGE eq "Use Overture.Functions.eq instead. Deprecated under #303." #-}

 open Image_∋_

 Range : (A → B) → Pred B (a ⊔ b)
 Range f b = ∃[ a ∈ A ] (f a) ≡ b

 range : (A → B) → Type (a ⊔ b)
 range f = Σ[ b ∈ B ] ∃[ a ∈ A ] (f a) ≡ b

 Image⊆Range : (f : A → B) → ∀ b → Image f ∋ b → b ∈ Range f
 Image⊆Range f b (eq a x) = a , (sym x)

 Range⊆Image : (f : A → B) → ∀ b → b ∈ Range f → Image f ∋ b
 Range⊆Image f b (a , x) = eq a (sym x)

 Imagef∋f : {f : A → B}{a : A} → Image f ∋ (f a)
 Imagef∋f = eq _ refl

 f∈range : {f : A → B}(a : A) → range f
 f∈range {f} a = (f a) , (a , refl)

An inhabitant of Image f ∋ b is a dependent pair (a , p), where a : A and p : b ≡ f a is a proof that f maps a to b. Since the proof that b belongs to the image of f is always accompanied by a witness a : A, we can actually compute a (pseudo)inverse of f. For convenience, we define this inverse function, which we call Inv, and which takes an arbitrary b : B and a (witness, proof)-pair, (a , p) : Image f ∋ b, and returns the witness a.

 Inv : (f : A → B){b : B} → Image f ∋ b  →  A
 Inv f (eq a _) = a

 {-# WARNING_ON_USAGE Inv "Use Overture.Functions.Inv instead. Deprecated under #303." #-}

 [_]⁻¹ : (f : A → B) → range f →  A
 [ f ]⁻¹ (_ , (a , _)) = a

We can prove that Inv f is the (range-restricted) right-inverse of f, as follows.

 InvIsInverseʳ : {f : A → B}{b : B}(q : Image f ∋ b) → f(Inv f q) ≡ b
 InvIsInverseʳ (eq _ p) = sym p

 {-# WARNING_ON_USAGE InvIsInverseʳ "Use Overture.Functions.InvIsInverseʳ instead. Deprecated under #303." #-}

 ⁻¹IsInverseʳ : {f : A → B}{bap : range f} → f ([ f ]⁻¹ bap) ≡ ∣ bap ∣
 ⁻¹IsInverseʳ {bap = (_ , (_ , p))} = p

Of course, the "range-restricted" qualifier is needed because Inf f is not defined outside the range of f.

In a certain sense, Inv f is also a (range-restricted) left-inverse.

 InvIsInverseˡ : ∀ {f a} → Inv f {b = f a} Imagef∋f ≡ a
 InvIsInverseˡ = refl

 ⁻¹IsInverseˡ : ∀ {f a} → [ f ]⁻¹ (f∈range a) ≡ a
 ⁻¹IsInverseˡ = refl