------------------------------------------------------------------------ -- The Agda standard library -- -- Injections ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} -- Note: use of the standard function hierarchy is encouraged. The -- module `Function` re-exports `Injective`, `IsInjection` and -- `Injection`. The alternative definitions found in this file will -- eventually be deprecated. module Function.Injection where open import Function as Fun using () renaming (_∘_ to _⟨∘⟩_) open import Level open import Relation.Binary open import Function.Equality as F using (_⟶_; _⟨$⟩_ ; Π) renaming (_∘_ to _⟪∘⟫_) open import Relation.Binary.PropositionalEquality as P using (_≡_) ------------------------------------------------------------------------ -- Injective functions Injective : ∀ {a₁ a₂ b₁ b₂} {A : Setoid a₁ a₂} {B : Setoid b₁ b₂} → A ⟶ B → Set _ Injective {A = A} {B} f = ∀ {x y} → f ⟨$⟩ x ≈₂ f ⟨$⟩ y → x ≈₁ y where open Setoid A renaming (_≈_ to _≈₁_) open Setoid B renaming (_≈_ to _≈₂_) ------------------------------------------------------------------------ -- The set of all injections between two setoids record Injection {f₁ f₂ t₁ t₂} (From : Setoid f₁ f₂) (To : Setoid t₁ t₂) : Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where field to : From ⟶ To injective : Injective to open Π to public ------------------------------------------------------------------------ -- The set of all injections from one set to another (i.e. injections -- with propositional equality) infix 3 _↣_ _↣_ : ∀ {f t} → Set f → Set t → Set _ From ↣ To = Injection (P.setoid From) (P.setoid To) injection : ∀ {f t} {From : Set f} {To : Set t} → (to : From → To) → (∀ {x y} → to x ≡ to y → x ≡ y) → From ↣ To injection to injective = record { to = P.→-to-⟶ to ; injective = injective } ------------------------------------------------------------------------ -- Identity and composition. infixr 9 _∘_ id : ∀ {s₁ s₂} {S : Setoid s₁ s₂} → Injection S S id = record { to = F.id ; injective = Fun.id } _∘_ : ∀ {f₁ f₂ m₁ m₂ t₁ t₂} {F : Setoid f₁ f₂} {M : Setoid m₁ m₂} {T : Setoid t₁ t₂} → Injection M T → Injection F M → Injection F T f ∘ g = record { to = to f ⟪∘⟫ to g ; injective = (λ {_} → injective g) ⟨∘⟩ injective f } where open Injection
Generated from commit 2fd14c996b195ef101dff8919e837907ca0a08aa.