 ### Injective functions

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

We say that a function `f : A → B` is injective (or monic) if it does not map two distinct elements of the domain to the same point in the codomain. The following type manifests this property.

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

module Base.Overture.Injective where

-- Imports from Agda and the Agda Standard Library ---------------------------------------------
open import Agda.Primitive   using ( _⊔_ ; Level ) renaming ( Set to Type )
open import Function.Bundles                      using ( _↣_ )
open import Function.Construct.Identity           using ( id-↣ )
open import Function.Base                         using ( _∘_ )
open import Function.Definitions as FD            using ( Injective )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )
open import Relation.Binary  using ( Rel )

private variable α β γ ℓ₁ ℓ₂ ℓ₃ : Level

id-is-injective : {A : Type α} → A ↣ A
id-is-injective {A = A} = id-↣ A

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

IsInjective : (A → B) → Type (α ⊔ β)
IsInjective f = Injective _≡_ _≡_ f

```

Next, we prove that the composition of injective functions is injective.

```∘-injective : {A : Type α}{B : Type β}{C : Type γ}{f : A → B}{g : B → C}
→           IsInjective f → IsInjective g → IsInjective (g ∘ f)
∘-injective fi gi = λ x → fi (gi x)

```