Agda UALib β

### Inverses

This is the Overture.Inverses module of the Agda Universal Algebra Library.

```
{-# OPTIONS --without-K --exact-split --safe #-}

module Overture.Inverses where

open import Overture.FunExtensionality public

open import MGS-Embeddings
using (equivs-are-embeddings; invertible; invertibles-are-equivs) public

```

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

```
module _ {A : π€ Μ }{B : π¦ Μ } where

data Image_β_ (f : A β B) : B β π€ β π¦ Μ
where
im : (x : A) β Image f β f x
eq : (b : B) β (a : A) β b β‘ f a β Image f β b

```

Next we verify that the type behaves as we expect.

```
ImageIsImage : (f : A β B)(b : B)(a : A) β b β‘ f a β Image f β b
ImageIsImage f b a bβ‘fa = eq b a bβ‘fa

```

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 {.(f a)} (im a) = a
Inv f (eq _ a _) = a

```

We can prove that `Inv f` is the right-inverse of `f`, as follows.

```
InvIsInv : (f : A β B){b : B}(q : Image f β b) β f(Inv f q) β‘ b
InvIsInv f {.(f a)} (im a) = refl
InvIsInv f (eq _ _ p) = p β»ΒΉ

```

#### Epics (surjective functions)

An epic (or surjective) function from `A` to `B` is as an inhabitant of the `Epic` type, which we now define.

```
Epic : (A β B) β  π€ β π¦ Μ
Epic f = β y β Image f β y

```

With the next definition, we can represent the right-inverse of an epic function.

```
EpicInv : (f : A β B) β Epic f β B β A
EpicInv f fE b = Inv f (fE b)

```

The right-inverse of `f` is obtained by applying `EpicInv` to `f` and a proof of `Epic f`. To see that this does indeed give the right-inverse we prove the `EpicInvIsRightInv` lemma below. This requires function composition, denoted `β` and defined in the Type Topology library.

```
module hide-β {A : π€ Μ}{B : π¦ Μ}{C : B β π¦ Μ } where

_β_ : Ξ  C β (f : A β B) β (x : A) β C (f x)
g β f = Ξ» x β g (f x)

open import MGS-MLTT using (_β_) public

```

Note that the next proof requires function extensionality, which we postulate in the module declaration.

```
module _ {fe : funext π¦ π¦}{A : π€ Μ}{B : π¦ Μ} where

EpicInvIsRightInv : (f : A β B)(fE : Epic f) β f β (EpicInv f fE) β‘ ππ B
EpicInvIsRightInv f fE = fe (Ξ» x β InvIsInv f (fE x))

```

We can also prove the following composition law for epics.

```
epic-factor : {C : π© Μ}(f : A β B)(g : A β C)(h : C β B)
β            f β‘ h β g β Epic f β Epic h

epic-factor f g h compId fe y = Ξ³
where
finv : B β A
finv = EpicInv f fe

ΞΆ : f (finv y) β‘ y
ΞΆ = cong-app (EpicInvIsRightInv f fe) y

Ξ· : (h β g) (finv y) β‘ y
Ξ· = (cong-app (compId β»ΒΉ)(finv y)) β ΞΆ

Ξ³ : Image h β y
Ξ³ = eq y (g (finv y)) (Ξ· β»ΒΉ)

```

#### Monics (injective functions)

We say that a function `f : A β B` is monic (or injective) if it does not map distinct elements to a common point. This following type manifests this property.

```
module _ {A : π€ Μ}{B : π¦ Μ} where

Monic : (f : A β B) β π€ β π¦ Μ
Monic f = β x y β f x β‘ f y β x β‘ y

```

Again, we obtain a pseudoinverse. Here it is obtained by applying the function `MonicInv` to `g` and a proof that `g` is monic.

```
MonicInv : (f : A β B) β Monic f β (b : B) β Image f β b β A
MonicInv f _ = Ξ» b imfb β Inv f imfb

```

The function defined by `MonicInv f fM` is the left-inverse of `f`.

```
MonicInvIsLeftInv : {f : A β B}{fM : Monic f}{x : A} β (MonicInv f fM)(f x)(im x) β‘ x
MonicInvIsLeftInv = refl

```

#### Embeddings

The `is-embedding` type is defined in the Type Topology library in the following way.

```module hide-is-embedding{A : π€ Μ}{B : π¦ Μ} where

is-embedding : (A β B) β π€ β π¦ Μ
is-embedding f = β b β is-subsingleton (fiber f b)

open import MGS-Embeddings using (is-embedding) public

```

Thus, `is-embedding f` asserts that `f` is a function all of whose fibers are subsingletons. Observe that an embedding is not simply an injective map. However, if we assume that the codomain `B` has unique identity proofs (UIP), then we can prove that a monic function into `B` is an embedding. We will do exactly that in the Relations.Truncation module when we take up the topic of sets and the UIP.

Finding a proof that a function is an embedding isnβt always easy, but one path that is often straightforward is to first prove that the function is invertible and then invoke the following theorem.

```
module _ {A : π€ Μ}{B : π¦ Μ} where

invertibles-are-embeddings : (f : A β B) β invertible f β is-embedding f
invertibles-are-embeddings f fi = equivs-are-embeddings f (invertibles-are-equivs f fi)

```

Finally, embeddings are monic; from a proof `p : is-embedding f` that `f` is an embedding we can construct a proof of `Monic f`. We confirm this as follows.

```
embedding-is-monic : (f : A β B) β is-embedding f β Monic f
embedding-is-monic f femb x y fxfy = ap prβ ((femb (f x)) fx fy)
where
fx fy : fiber f (f x)
fx = x , refl
fy = y , (fxfy β»ΒΉ)

```