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}