Martin Escardo 7th December 2018.

We show that the natural map into the lifting is an embedding using
the structure identity principle. A more direct, but longer, proof
is in the module LiftingEmbeddingDirectly.

\begin{code}

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

open import SpartanMLTT

module LiftingEmbeddingViaSIP
        (𝓣 𝓤 : Universe)
        (X : 𝓤 ̇ )
       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-EquivalenceExamples
open import UF-FunExt
open import UF-Univalence
open import UF-UA-FunExt

open import Lifting 𝓣
open import LiftingIdentityViaSIP 𝓣

\end{code}

The crucial point the use the characterization of identity via the
structure identity principle:

\begin{code}

η-is-embedding' : is-univalent 𝓣 → funext 𝓣 𝓤 → is-embedding (η {𝓤} {X})
η-is-embedding' ua fe = embedding-criterion' η c
 where
  a = (𝟙 ≃ 𝟙) ≃⟨ ≃-sym (univalence-≃ ua 𝟙 𝟙) ⟩
      (𝟙 ≡ 𝟙) ≃⟨ 𝟙-≡-≃ 𝟙 (univalence-gives-funext ua)
                         (univalence-gives-propext ua) 𝟙-is-prop ⟩
      𝟙       ■

  b = λ x y → ((λ _ → x) ≡ (λ _ → y)) ≃⟨ ≃-funext fe (λ _ → x) (λ _ → y) ⟩
              (𝟙 → x ≡ y)             ≃⟨ ≃-sym (𝟙→ fe) ⟩
              (x ≡ y)                 ■

  c = λ x y → (η x ≡ η y)                       ≃⟨ 𝓛-Id ua (η x) (η y) ⟩
              (𝟙 ≃ 𝟙) × ((λ _ → x) ≡ (λ _ → y)) ≃⟨ ×-cong a (b x y) ⟩
              𝟙 × (x ≡ y)                       ≃⟨ 𝟙-lneutral ⟩
              (x ≡ y)                           ■

\end{code}