------------------------------------------------------------------------
-- Embeddings
------------------------------------------------------------------------

-- Partially following the HoTT book.

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

open import Equality

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

open import Logical-equivalence using (_⇔_)
open import Prelude as P hiding (id) renaming (_∘_ to _⊚_)

open import Bijection eq using (_↔_)
open Derived-definitions-and-properties eq
open import Equivalence eq as Eq hiding (id; _∘_)
open import H-level eq
open import H-level.Closure eq
open import Injection eq as Injection using (Injective; _↣_)
open import Preimage eq using (_⁻¹_)

------------------------------------------------------------------------
-- Embeddings

-- The property of being an embedding.

Is-embedding :  {a b} {A : Set a} {B : Set b}  (A  B)  Set (a  b)
Is-embedding f =  x y  Is-equivalence (cong f {x = x} {y = y})

-- Is-embedding is propositional (assuming extensionality).

Is-embedding-propositional :
   {a b} 
  Extensionality (a  b) (a  b) 
   {A : Set a} {B : Set b} {f : A  B} 
  Is-proposition (Is-embedding f)
Is-embedding-propositional {b = b} ext =
  Π-closure (lower-extensionality b lzero ext) 1 λ _ 
  Π-closure (lower-extensionality b lzero ext) 1 λ _ 
  Eq.propositional ext _

-- Embeddings.

record Embedding {f t} (From : Set f) (To : Set t) : Set (f  t) where
  field
    to           : From  To
    is-embedding : Is-embedding to

  equivalence :  {x y}  (x  y)  (to x  to y)
  equivalence =  _ , is-embedding _ _ 

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

-- Embedding is a preorder.

id :  {a} {A : Set a}  Embedding A A
id {A = A} = record
  { to           = P.id
  ; is-embedding = λ x y 
      Eq.respects-extensional-equality
        cong-id
        (singleton-contractible {A = x  y})
  }

infixr 9 _∘_

_∘_ :  {a b c} {A : Set a} {B : Set b} {C : Set c} 
      Embedding B C  Embedding A B  Embedding A C
f  g = record
  { to           = to f  to g
  ; is-embedding = λ _ _ 
      Eq.respects-extensional-equality
        (cong-∘ (to f) (to g))
        (Two-out-of-three.f-g
           (two-out-of-three _ _)
           (is-embedding g _ _) (is-embedding f _ _))
  }
  where
  open Embedding

------------------------------------------------------------------------
-- Preimages

-- If f is an embedding, then f ⁻¹ y is propositional.
--
-- This result is taken (perhaps with some changes) from the proof of
-- Theorem 4.6.3 in the HoTT book (first edition).

embedding→⁻¹-propositional :
   {a b} {A : Set a} {B : Set b} {f : A  B} 
  Is-embedding f 
   y  Is-proposition (f ⁻¹ y)
embedding→⁻¹-propositional {f = f} is-emb y =
  _⇔_.from propositional⇔irrelevant
    λ { (x₁ , eq₁) (x₂ , eq₂) 
        let
          equiv : (x₁  x₂)  (f x₁  f x₂)
          equiv =  _ , is-emb _ _ 

          x₁≡x₂ : x₁  x₂
          x₁≡x₂ = _≃_.from equiv
            (f x₁  ≡⟨ eq₁ 
             y     ≡⟨ sym eq₂ ⟩∎
             f x₂  )
        in
        Σ-≡,≡→≡
          x₁≡x₂
          (subst  z  f z  y) x₁≡x₂ eq₁              ≡⟨ subst-∘ (_≡ y) f x₁≡x₂ 
           subst (_≡ y) (cong f x₁≡x₂) eq₁              ≡⟨ cong  eq  subst (_≡ y) eq eq₁) $ sym $ sym-sym (cong f x₁≡x₂) 
           subst (_≡ y) (sym $ sym $ cong f x₁≡x₂) eq₁  ≡⟨ subst-trans (sym $ cong f x₁≡x₂) 
           trans (sym $ cong f x₁≡x₂) eq₁               ≡⟨ cong  eq  trans (sym eq) eq₁) $ _≃_.right-inverse-of equiv _ 
           trans (sym $ trans eq₁ (sym eq₂)) eq₁        ≡⟨ cong (flip trans eq₁) $ sym-trans eq₁ (sym eq₂) 
           trans (trans (sym (sym eq₂)) (sym eq₁)) eq₁  ≡⟨ trans-[trans-sym]- _ eq₁ 
           sym (sym eq₂)                                ≡⟨ sym-sym _ ⟩∎
           eq₂                                          ) }

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

-- Functions that are embeddings are injective.

injective :  {a b} {A : Set a} {B : Set b} {f : A  B} 
            Is-embedding f  Injective f
injective is-emb = _≃_.from  _ , is-emb _ _ 

-- Embeddings are injections.

injection :  {a b} {A : Set a} {B : Set b}  Embedding A B  A  B
injection f = record
  { to        = Embedding.to f
  ; injective = injective (Embedding.is-embedding f)
  }

private

  -- If the domain of f is a set, then Injective f is propositional
  -- (assuming extensionality).

  Injective-propositional :
     {a b} 
    Extensionality (a  b) (a  b) 
     {A : Set a} {B : Set b} {f : A  B} 
    Is-set A  Is-proposition (Injective f)
  Injective-propositional {a} {b} ext A-set =
    implicit-Π-closure (lower-extensionality b lzero ext) 1 λ _ 
    implicit-Π-closure (lower-extensionality b lzero ext) 1 λ _ 
    Π-closure (lower-extensionality a b ext)              1 λ _ 
    A-set _ _

-- For functions between sets the property of being injective is
-- equivalent to the property of being an embedding (assuming
-- extensionality).

Injective≃Is-embedding :
   {a b} {A : Set a} {B : Set b} 
  Extensionality (a  b) (a  b) 
  Is-set A  Is-set B 
  (f : A  B)  Injective f  Is-embedding f
Injective≃Is-embedding ext A-set B-set f =
  _↔_.to
    (⇔↔≃ ext
         (Injective-propositional ext A-set)
         (Is-embedding-propositional ext))
    (record { to   = λ cong-f⁻¹ _ _ 
                         _≃_.is-equivalence $
                         _↔_.to (⇔↔≃ ext (A-set _ _) (B-set _ _))
                                (record { from = cong-f⁻¹ })
            ; from = injective
            })

-- If A and B are sets, then the type of injections from A to B is
-- isomorphic to the type of embeddings from A to B (assuming
-- extensionality).

↣↔Embedding :
   {a b} {A : Set a} {B : Set b} 
  Extensionality (a  b) (a  b) 
  Is-set A  Is-set B 
  (A  B)  Embedding A B
↣↔Embedding {A = A} {B} ext A-set B-set = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ f  record
                 { to           = _↣_.to f
                 ; is-embedding =
                     _≃_.to (Injective≃Is-embedding ext A-set B-set _)
                            (_↣_.injective f)
                 }
      ; from = injection
      }
    ; right-inverse-of = λ f 
        cong (uncurry λ to (emb : Is-embedding to) 
                        record { to = to; is-embedding = emb })
             (Σ-≡,≡→≡ (refl _)
                      (_⇔_.to propositional⇔irrelevant
                         (Is-embedding-propositional ext) _ _))
    }
  ; left-inverse-of = λ f 
      cong (uncurry λ to (inj : Injective to) 
                      record { to = to; injective = inj })
           (Σ-≡,≡→≡ (refl _)
                    (_⇔_.to propositional⇔irrelevant
                       (Injective-propositional ext A-set) _ _))
  }