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)