Martin Escardo 25th October 2018.

We show that the natural map into the lifting is an embedding.  See
the module Lifting.EmbeddingViaSIP for an alternative approach via the
structure identity principle.

\begin{code}

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

open import MLTT.Spartan

module Lifting.EmbeddingDirectly (𝓣 : Universe) where

open import UF.Base
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.Embeddings
open import UF.Equiv
open import UF.FunExt

open import Lifting.Construction 𝓣

\end{code}

Our strategy here to show that Ξ· is an embedding (has subsingleton
fibers) is to exhibit it as the composite of two embeddings (the first
of which is actually an equivalence).

\begin{code}

π“š : 𝓀 Μ‡ β†’ 𝓀 βŠ” 𝓣 ⁺ Μ‡
π“š X = Ξ£ P κž‰ 𝓣 Μ‡ , (P β†’ X) Γ— is-singleton P

ΞΊ : {X : 𝓀 Μ‡ } β†’ X β†’ π“š X
ΞΊ x = πŸ™ , (Ξ» _ β†’ x) , πŸ™-is-singleton

ΞΆ : (X : 𝓀 Μ‡ ) (P : 𝓣 Μ‡ ) β†’ (P β†’ X) Γ— is-singleton P β†’ (P β†’ X) Γ— is-prop P
ΞΆ X P (Ο† , i) = Ο† , singletons-are-props i

π“šβ†’π“› : (X : 𝓀 Μ‡ ) β†’ π“š X β†’ 𝓛 X
π“šβ†’π“› X = NatΞ£ (ΞΆ X)

Ξ·-composite : funext 𝓣 𝓣
            β†’ funext 𝓀 (𝓣 ⁺ βŠ” 𝓀)
            β†’ {X : 𝓀 Μ‡ } β†’ Ξ· ＝ π“šβ†’π“› X ∘ ΞΊ
Ξ·-composite fe fe' {X} = dfunext fe' h
 where
  h : (x : X)
    β†’ (πŸ™ , (Ξ» _ β†’ x) , πŸ™-is-prop)
    ＝ (πŸ™ , (Ξ» _ β†’ x) , singletons-are-props (πŸ™-is-singleton))
  h x = to-Ξ£-＝ (refl , to-Γ—-＝ refl (being-prop-is-prop fe _ _))

\end{code}

The fact that π“šβ†’π“› is an embedding can be proved by obtaining it as
a combination of maps that we already know to be embeddings, using
Γ—-embedding, maps-of-props-are-embeddings, id-is-embedding, and
NatΞ£-embedding.:

\begin{code}

ΞΆ-is-embedding : funext 𝓣 𝓣 β†’ (X : 𝓀 Μ‡ ) (P : 𝓣 Μ‡ ) β†’ is-embedding (ΞΆ X P)
ΞΆ-is-embedding fe X P = Γ—-is-embedding
                         id
                         singletons-are-props
                         id-is-embedding
                         (maps-of-props-are-embeddings
                           singletons-are-props
                           (being-singleton-is-prop fe)
                           (being-prop-is-prop fe))

π“šβ†’π“›-is-embedding : funext 𝓣 𝓣 β†’ (X : 𝓀 Μ‡ ) β†’ is-embedding (π“šβ†’π“› X)
π“šβ†’π“›-is-embedding fe X = NatΞ£-is-embedding
                          (Ξ» P β†’ (P β†’ X) Γ— is-singleton P)
                          (Ξ» P β†’ (P β†’ X) Γ— is-prop P)
                          (ΞΆ X)
                          (ΞΆ-is-embedding fe X)
\end{code}

That ΞΊ is an equivalence corresponds to the fact that the lifting of a
type X with respect to the dominance "is-singleton" is equivalent to X
itself.

\begin{code}

ΞΊ-is-equiv : propext 𝓣
           β†’ funext 𝓣 𝓣
           β†’ funext 𝓣 𝓀
           β†’ {X : 𝓀 Μ‡ } β†’ is-equiv (ΞΊ {𝓀} {X})
ΞΊ-is-equiv {𝓀} pe fe fe' {X} = qinvs-are-equivs ΞΊ (ρ , (ρκ , κρ))
 where
  ρ : {X : 𝓀 Μ‡ } β†’ π“š X β†’ X
  ρ (P , Ο† , i) = Ο† (center i)

  ρκ : {X : 𝓀 Μ‡ } (x : X) β†’ ρ (ΞΊ x) ＝ x
  ρκ x = refl

  κρ : (m : π“š X) β†’ ΞΊ (ρ m) ＝ m
  κρ (P , Ο† , i) = u
   where
    t : πŸ™ ＝ P
    t = pe πŸ™-is-prop
           (singletons-are-props i)
           (Ξ» _ β†’ center i)
           unique-to-πŸ™

    s : (t : πŸ™ ＝ P)
      β†’ transport (Ξ» - β†’ (- β†’ X) Γ— is-singleton -) t ((Ξ» _ β†’ Ο† (center i)) ,
        πŸ™-is-singleton)
      ＝ Ο† , i
    s refl = to-Γ—-＝ a b
     where
      a : (Ξ» x β†’ Ο† (center i)) ＝ Ο†
      a = dfunext fe' (Ξ» x β†’ ap Ο† (πŸ™-is-prop (center i) x))

      b : πŸ™-is-singleton ＝ i
      b = (singletons-are-props
            (pointed-props-are-singletons
            πŸ™-is-singleton (being-singleton-is-prop fe))
            πŸ™-is-singleton i)

    u : πŸ™ , (Ξ» _ β†’ Ο† (center i)) , πŸ™-is-singleton ＝ P , Ο† , i
    u = to-Σ-＝ (t , s t)

ΞΊ-is-embedding : propext 𝓣
               β†’ funext 𝓣 𝓣
               β†’ funext 𝓣 𝓀
               β†’ {X : 𝓀 Μ‡ } β†’ is-embedding (ΞΊ {𝓀} {X})
ΞΊ-is-embedding pe fe fe' = equivs-are-embeddings ΞΊ (ΞΊ-is-equiv pe fe fe')

\end{code}

Finally, Ξ· is an embedding because it is equal to the composition of
two embeddings:

\begin{code}

Ξ·-is-embedding : propext 𝓣
               β†’ funext 𝓣 𝓣
               β†’ funext 𝓣 𝓀
               β†’ funext 𝓀 (𝓣 ⁺ βŠ” 𝓀)
               β†’ {X : 𝓀 Μ‡ } β†’ is-embedding (Ξ· {𝓀} {X})
Ξ·-is-embedding pe fe fe' fe'' {X} =
 transport⁻¹
  is-embedding
  (Ξ·-composite fe fe'')
  (∘-is-embedding (ΞΊ-is-embedding pe fe fe') (π“šβ†’π“›-is-embedding fe X))

\end{code}