↑ Top


Injective functions

This is the [Base.Functions.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.Functions.Injective where

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

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)

← Base.Functions.FuncInverses Base.Functions.Surjective →