------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties for injections
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Function.Properties.Injection where
open import Function.Definitions using (Injective)
open import Function.Bundles using (Injection; Func; _⟶_; _↣_)
import Function.Construct.Identity as Identity using (injection)
import Function.Construct.Composition as Compose using (injection)
open import Level using (Level)
open import Data.Product.Base using (proj₁; proj₂)
open import Relation.Binary.Definitions
open import Relation.Binary using (Setoid)
private
variable
a b c ℓ ℓ₁ ℓ₂ ℓ₃ : Level
A B : Set a
T S U : Setoid a ℓ
------------------------------------------------------------------------
-- Constructors
mkInjection : (f : Func S T) (open Func f) →
Injective Eq₁._≈_ Eq₂._≈_ to →
Injection S T
mkInjection f injective = record
{ Func f
; injective = injective
}
------------------------------------------------------------------------
-- Conversion functions
↣⇒⟶ : A ↣ B → A ⟶ B
↣⇒⟶ = Injection.function
------------------------------------------------------------------------
-- Setoid properties
refl : Reflexive (Injection {a} {ℓ})
refl {x = x} = Identity.injection x
trans : Trans (Injection {a} {ℓ₁} {b} {ℓ₂})
(Injection {b} {ℓ₂} {c} {ℓ₃})
(Injection {a} {ℓ₁} {c} {ℓ₃})
trans = Compose.injection
------------------------------------------------------------------------
-- Propositonal properties
↣-refl : Injection S S
↣-refl = refl
↣-trans : Injection S T → Injection T U → Injection S U
↣-trans = trans
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4