Martin Escardo 7th December 2018.

Characterization of equality in the lifting via the structure of
identity principle.

\begin{code}

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

open import MLTT.Spartan

module Lifting.IdentityViaSIP
        (𝓣 : Universe)
        {𝓀 : Universe}
        {X : 𝓀 Μ‡ }
       where

open import UF.Base
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.FunExt
open import UF.Univalence
open import UF.UA-FunExt
open import UF.StructureIdentityPrinciple

open import Lifting.Construction 𝓣

_⋍_ : 𝓛 X β†’ 𝓛 X β†’ 𝓣 βŠ” 𝓀 Μ‡
l ⋍ m = Ξ£ e κž‰ is-defined l ≃ is-defined m , value l ＝ value m ∘ ⌜ e ⌝

𝓛-Id : is-univalent 𝓣 β†’ (l m : 𝓛 X) β†’ (l ＝ m) ≃ (l ⋍ m)
𝓛-Id ua = ＝-is-≃ₛ'
 where
  open gsip-with-axioms'
        𝓣 (𝓣 βŠ” 𝓀) (𝓣 βŠ” 𝓀) 𝓣 ua
        (Ξ» P β†’ P β†’ X)
        (Ξ» P s β†’ is-prop P)
        (Ξ» P s β†’ being-prop-is-prop (univalence-gives-funext ua))
        (Ξ» {l m (f , e) β†’ prβ‚‚ l ＝ prβ‚‚ m ∘ f})
        (Ξ» l β†’ refl)
        (Ξ» P Ξ΅ Ξ΄ β†’ id)
        (Ξ» A Ο„ Ο… β†’ refl-left-neutral)

⋍-gives-＝ : is-univalent 𝓣 β†’ {l m : 𝓛 X} β†’ (l ⋍ m) β†’ l ＝ m
⋍-gives-＝ ua = ⌜ 𝓛-Id ua _ _ ⌝⁻¹

\end{code}

When dealing with functions it is often more convenient to work with
pointwise equality, and hence we also consider:

\begin{code}

_⋍·_ : 𝓛 X β†’ 𝓛 X β†’ 𝓣 βŠ” 𝓀 Μ‡
l ⋍· m = Ξ£ e κž‰ is-defined l ≃ is-defined m , value l ∼ value m ∘ ⌜ e ⌝

is-defined-⋍· : (l m : 𝓛 X)
              β†’ l ⋍· m β†’ is-defined l ≃ is-defined m
is-defined-⋍· l m = pr₁

value-⋍· : (l m : 𝓛 X) (𝕗 : l ⋍· m)
         β†’ value l ∼ (Ξ» x β†’ value m (⌜ is-defined-⋍· l m 𝕗 ⌝ x))
value-⋍· l m = prβ‚‚

Id-to-⋍· : (l m : 𝓛 X) β†’ (l ＝ m) β†’ (l ⋍· m)
Id-to-⋍· l m refl = (≃-refl (is-defined l)) , (Ξ» x β†’ refl)

𝓛-IdΒ· : is-univalent 𝓣
      β†’ funext 𝓣 𝓀
      β†’ (l m : 𝓛 X) β†’ (l ＝ m) ≃ (l ⋍· m)
𝓛-IdΒ· ua fe l m = (𝓛-Id ua l m)
                ● (Ξ£-cong (Ξ» e β†’ ≃-funext fe (value l) (value m ∘ ⌜ e ⌝)))

⋍·-gives-＝ : is-univalent 𝓣
           β†’ funext 𝓣 𝓀
           β†’ {l m : 𝓛 X} β†’ (l ⋍· m) β†’ l ＝ m
⋍·-gives-＝ ua fe = ⌜ 𝓛-IdΒ· ua fe _ _ ⌝⁻¹

\end{code}

Added 8th September 2025.

\begin{code}

⋍·-refl : (l : 𝓛 X) β†’ l ⋍· l
⋍·-refl l = ≃-refl _ , ∼-refl

⋍·-sym : (l m : 𝓛 X) β†’ l ⋍· m β†’ m ⋍· l
⋍·-sym l m (e , d) =
 ≃-sym e ,
 Ξ» p β†’
  value m p                   ＝⟨ ap (value m) ((inverses-are-sections' e p)⁻¹) ⟩
  value m (⌜ e ⌝ (⌜ e ⌝⁻¹ p)) ＝⟨ (d (⌜ e ⌝⁻¹ p))⁻¹ ⟩
  value l (⌜ e ⌝⁻¹ p)         ∎

⋍·-trans : (l m n : 𝓛 X) β†’ l ⋍· m β†’ m ⋍· n β†’ l ⋍· n
⋍·-trans l m n (e , d) (e' , d') =
 (e ● e') ,
 (Ξ» p β†’ value l p                  ＝⟨ d p ⟩
        value m (⌜ e ⌝ p)          ＝⟨ d' (⌜ e ⌝ p) ⟩
        value n (⌜ e' ⌝ (⌜ e ⌝ p)) ＝⟨refl⟩
        value n (⌜ e ● e' ⌝ p)     ∎)

\end{code}