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.


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

open import SpartanMLTT

module LiftingEmbeddingViaSIP
        (𝓣 𝓤 : Universe)
        (X : 𝓤 ̇ )

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 𝓣


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


η-is-embedding' : is-univalent 𝓣  funext 𝓣 𝓤  is-embedding (η {𝓤} {X})
η-is-embedding' ua fe = embedding-criterion' η c
  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)