 Inverses

This is the Overture.Inverses module of the agda-algebras library.

{-# OPTIONS --without-K --exact-split --safe #-}
module Overture.Inverses where

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

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

private variable α β : Level

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

module _ {A : Type α }{B : Type β } where

data Image_∋_ (f : A  B) : B  Type (α  β) where
eq : {b : B}  (a : A)  b  f a  Image f  b

open Image_∋_

Range : (A  B)  Pred B (α  β)
Range f b = ∃[ a  A ] (f a)  b

range : (A  B)  Type (α  β)
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

[_]⁻¹ : (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

⁻¹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