↑ Top


Inverses

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

{-# OPTIONS --without-K --exact-split --safe #-}
module Base.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 Base.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


← Base.Overture.Preliminaries Base.Overture.Injective →