------------------------------------------------------------------------
-- Injections
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Equality

module Injection
  {reflexive} (eq :  {a p}  Equality-with-J a p reflexive) where

open Derived-definitions-and-properties eq
open import Prelude as P hiding (id) renaming (_∘_ to _⊚_)

------------------------------------------------------------------------
-- Injections

-- The property of being injective.

Injective :  {a b} {A : Set a} {B : Set b}  (A  B)  Set (a  b)
Injective f =  {x y}  f x  f y  x  y

infix 0 _↣_

-- Injections.

record _↣_ {f t} (From : Set f) (To : Set t) : Set (f  t) where
  field
    to        : From  To
    injective : Injective to

------------------------------------------------------------------------
-- Preorder

-- _↣_ is a preorder.

id :  {a} {A : Set a}  A  A
id = record
  { to        = P.id
  ; injective = P.id
  }

infixr 9 _∘_

_∘_ :  {a b c} {A : Set a} {B : Set b} {C : Set c} 
      B  C  A  B  A  C
f  g = record
  { to        = to′
  ; injective = injective′
  }
  where
  open _↣_

  to′ = to f  to g

  abstract
    injective′ : Injective to′
    injective′ = injective g  injective f

-- "Equational" reasoning combinators.

infix  -1 finally-↣
infixr -2 step-↣

-- For an explanation of why step-↣ is defined in this way, see
-- Equality.step-≡.

step-↣ :  {a b c} (A : Set a) {B : Set b} {C : Set c} 
         B  C  A  B  A  C
step-↣ _ = _∘_

syntax step-↣ A B↣C A↣B = A ↣⟨ A↣B  B↣C

finally-↣ :  {a b} (A : Set a) (B : Set b)  A  B  A  B
finally-↣ _ _ A↣B = A↣B

syntax finally-↣ A B A↣B = A ↣⟨ A↣B ⟩□ B