Martin Escardo December 2018.

The lifting of a type forms a univalent pre-∞-category with hom types
l βŠ‘ m, which is a partial order if the type is a set.

At the moment we don't have categories in this development, but this
doesn't prevent us from giving this particular example of a univalent
category.

\begin{code}

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

open import MLTT.Spartan

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

open import Lifting.IdentityViaSIP 𝓣
open import Lifting.Construction 𝓣
open import UF.Base
open import UF.Equiv
open import UF.Equiv-FunExt
open import UF.EquivalenceExamples
open import UF.FunExt
open import UF.Lower-FunExt
open import UF.Sets
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.UA-FunExt
open import UF.Univalence

\end{code}

We define l βŠ‘ m to mean that if l is defined then so is m with the
same value. Here the suffix "-pr" standands for preservation (and also
for projection!).

\begin{code}

_βŠ‘_ : 𝓛 X β†’ 𝓛 X β†’ 𝓀 βŠ” 𝓣 Μ‡
l βŠ‘ m = Ξ£ f κž‰ (is-defined l β†’ is-defined m) , value l ∼ value m ∘ f

def-pr : (l m : 𝓛 X) β†’ l βŠ‘ m β†’ (is-defined l β†’ is-defined m)
def-pr l m = pr₁

val-pr : (l m : 𝓛 X) (Ξ± : l βŠ‘ m) β†’ value l ∼ value m ∘ (def-pr l m Ξ±)
val-pr l m = prβ‚‚

dom : {l m : 𝓛 X} β†’ l βŠ‘ m β†’ 𝓛 X
dom {l} {m} Ξ± = l

cod : {l m : 𝓛 X} β†’ l βŠ‘ m β†’ 𝓛 X
cod {l} {m} Ξ± = m

𝓛-id : (l : 𝓛 X) β†’ l βŠ‘ l
𝓛-id l = id , (Ξ» x β†’ refl)

𝓛-Id-to-arrow : (l m : 𝓛 X) β†’ l ＝ m β†’ l βŠ‘ m
𝓛-Id-to-arrow l l refl = 𝓛-id l

𝓛-comp : (l m n : 𝓛 X) β†’ l βŠ‘ m β†’ m βŠ‘ n β†’ l βŠ‘ n
𝓛-comp l m n (f , Ξ΄) (g , Ξ΅) = g ∘ f , (Ξ» p β†’ Ξ΄ p βˆ™ Ξ΅ (f p))

𝓛-comp-unit-right : (l m : 𝓛 X) (Ξ± : l βŠ‘ m) β†’ 𝓛-comp l m m Ξ± (𝓛-id m) ＝ Ξ±
𝓛-comp-unit-right l m Ξ± = refl

𝓛-comp-unit-left : funext 𝓣 𝓀
                 β†’ (l m : 𝓛 X) (Ξ± : l βŠ‘ m)
                 β†’ 𝓛-comp l l m (𝓛-id l) Ξ± ＝ Ξ±
𝓛-comp-unit-left fe l m Ξ± = to-Ξ£-＝ (refl , dfunext fe Ξ» p β†’ refl-left-neutral)

𝓛-comp-assoc : funext 𝓣 𝓀
             β†’ {l m n o : 𝓛 X} (Ξ± : l βŠ‘ m) (Ξ² : m βŠ‘ n) (Ξ³ : n βŠ‘ o)
             β†’ 𝓛-comp l n o (𝓛-comp l m n Ξ± Ξ²) Ξ³
             ＝ 𝓛-comp l m o Ξ± (𝓛-comp m n o Ξ² Ξ³)
𝓛-comp-assoc fe (f , Ξ΄) (g , Ξ΅) (h , ΞΆ) =
 to-Ξ£-＝ (refl , dfunext fe (Ξ» p β†’ βˆ™assoc (Ξ΄ p) (Ξ΅ (f p)) (ΞΆ (g (f p)))))

\end{code}

Thus, the associativity law in this pre-∞-category is that of function
composition in the first component (where it hence holds
definitionally) and that of path composition in the first
component. (Hence this pre-∞-category should qualify as an ∞-category,
with all coherence laws satisfied automatically, except that there is
at present no definition of ∞-category in univalent type theory.)

If X is a set, then _βŠ‘_ is a partial order:

\begin{code}

βŠ‘-prop-valued : funext 𝓣 𝓣
              β†’ funext 𝓣 𝓀
              β†’ is-set X
              β†’ (l m : 𝓛 X) β†’ is-prop (l βŠ‘ m)
βŠ‘-prop-valued fe fe' s l m (f , Ξ΄) (g , Ξ΅) =
 to-Ξ£-＝ (dfunext fe (Ξ» p β†’ being-defined-is-prop m (f p) (g p)) ,
         Ξ -is-prop fe' (Ξ» d β†’ s) _ Ξ΅)

\end{code}

TODO. This order is directed complete (easy). We should also do least
fixed points of continuous maps.

This TODO was implemented by Tom de Jong in the file
DomainTheory.Lifting.LiftingSet.lagda.

Next we show that for any l : 𝓛 X,

 fiber Ξ· l ≃ is-defined l,

using the fact that the fiber is a proposition by virtue of Ξ· being an
embedding.

\begin{code}

βŠ‘-anti-lemma : propext 𝓣
             β†’ funext 𝓣 𝓣
             β†’ funext 𝓣 𝓀
             β†’ {l m : 𝓛 X} β†’ l βŠ‘ m β†’ (is-defined m β†’ is-defined l) β†’ l ＝ m
βŠ‘-anti-lemma pe fe fe' {Q , ψ , j} {P , Ο† , i} (f , Ξ΄) g = e
 where
  Ξ΅ : (p : P) β†’ ψ (g p) ＝ Ο† p
  Ξ΅ p = Ξ΄ (g p) βˆ™ ap Ο† (i (f (g p)) p)

  a : Q ＝ P
  a = pe j i f g

  b : Idtofun (a ⁻¹) ＝ g
  b = dfunext fe (Ξ» p β†’ j (Idtofun (a ⁻¹) p) (g p))

  c : transport (Ξ» - β†’ (- β†’ X) Γ— is-prop -) a (ψ , j)
    ＝[ (P β†’ X) Γ— is-prop P ]
     (transport (Ξ» - β†’ - β†’ X) a ψ , transport is-prop a j)
  c = transport-Γ— (Ξ» - β†’ - β†’ X) is-prop a

  d = pr₁ (transport (Ξ» - β†’ (- β†’ X) Γ— is-prop -) a (ψ , j)) ＝⟨ I ⟩
      transport (Ξ» - β†’ - β†’ X) a ψ                           ＝⟨ II ⟩
      ψ ∘ Idtofun (a ⁻¹)                                    ＝⟨ III ⟩
      ψ ∘ g                                                 ＝⟨ IV ⟩
      Ο†                                                     ∎
       where
        I   = ap pr₁ c
        II  = transport-is-pre-comp a ψ
        III = ap (Ξ» - β†’ ψ ∘ -) b
        IV  = dfunext fe' Ξ΅

  e : Q , ψ , j ＝ P , Ο† , i
  e = to-Ξ£-＝ (a , to-Γ—-＝ d (being-prop-is-prop fe _ i))

βŠ‘-anti : propext 𝓣
       β†’ funext 𝓣 𝓣
       β†’ funext 𝓣 𝓀
       β†’ {l m : 𝓛 X} β†’ (l βŠ‘ m) Γ— (m βŠ‘ l) β†’ l ＝ m
βŠ‘-anti pe fe fe' ((f , Ξ΄) , (g , Ξ΅)) = βŠ‘-anti-lemma pe fe fe' (f , Ξ΄) g

\end{code}

We can now establish the promised fact:

\begin{code}

open import Lifting.EmbeddingDirectly 𝓣

Ξ·-fiber-same-as-is-defined : propext 𝓣
                           β†’ funext 𝓣 𝓣
                           β†’ funext 𝓣 𝓀
                           β†’ funext 𝓀 (𝓣 ⁺ βŠ” 𝓀)
                           β†’ (l : 𝓛 X) β†’ (Ξ£ x κž‰ X , Ξ· x ＝ l) ≃ is-defined l
Ξ·-fiber-same-as-is-defined pe fe fe' fe'' l = qinveq (f l) (g l , gf , fg)
 where
  f : (l : 𝓛 X) β†’ fiber Ξ· l β†’ is-defined l
  f (.πŸ™ , .(Ξ» _ β†’ x) , .πŸ™-is-prop) (x , refl) = ⋆

  g : (l : 𝓛 X) β†’ is-defined l β†’ fiber Ξ· l
  g (P , Ο† , i) p = Ο† p , βŠ‘-anti pe fe fe' (a , b)
   where
    a : Ξ· (Ο† p) βŠ‘ (P , Ο† , i)
    a = (Ξ» _ β†’ p) , (Ξ» _ β†’ refl)

    b : (P , Ο† , i) βŠ‘ Ξ· (Ο† p)
    b = (Ξ» _ β†’ ⋆) , (Ξ» q β†’ ap Ο† (i q p))

  fg : (d : is-defined l) β†’ f l (g l d) ＝ d
  fg d = being-defined-is-prop l (f l (g l d)) d

  gf : (z : fiber Ξ· l) β†’ g l (f l z) ＝ z
  gf z = Ξ·-is-embedding pe fe fe' fe'' l (g l (f l z)) z

\end{code}

They can't be equal, in the absence of cumulativity (and propositional
resizing), as the lhs lives in a universe higher than the rhs, and
equality is well-typed only for elements of the same type (here of the
same universe). This can be seen by adding type annotations to the
formulation of the above equivalence:

\begin{code}

private
 Ξ·-fiber-same-as-is-defined' : propext 𝓣
                             β†’ funext 𝓣 𝓣
                             β†’ funext 𝓣 𝓀
                             β†’ funext 𝓀 (𝓣 ⁺ βŠ” 𝓀)
                             β†’ (l : 𝓛 X) β†’ (fiber Ξ· l    ∢ 𝓣 ⁺ βŠ” 𝓀 Μ‡ )
                                         ≃ (is-defined l ∢ 𝓣 Μ‡ )
 Ξ·-fiber-same-as-is-defined' = Ξ·-fiber-same-as-is-defined

\end{code}

For no choice of universes 𝓀 and 𝓣 can we have 𝓣 ⁺ βŠ” 𝓀 to coincide
with 𝓣. However, for some dominances other than is-prop, it is possible to
have the equality between the fiber of l and the definedness of l.

The following simplified proof of βŠ‘-anti uses the SIP via the
construction of _⋍·_ in another module:

\begin{code}

βŠ‘-anti-sip : is-univalent 𝓣
           β†’ funext 𝓣 𝓀
           β†’ {l m : 𝓛 X} β†’ (l βŠ‘ m) Γ— (m βŠ‘ l) β†’ l ＝ m
βŠ‘-anti-sip ua fe {Q , ψ , j} {P , Ο† , i} ((f , Ξ΄) , (g , Ξ΅)) =
 ⌜ 𝓛-IdΒ· ua fe (Q , ψ , j) (P , Ο† , i) ⌝⁻¹ Ξ³
 where
  e : Q ≃ P
  e = f , ((g , (Ξ» p β†’ i (f (g p)) p)) , (g , (Ξ» q β†’ j (g (f q)) q)))

  Ξ³ : (Q , ψ , j) ⋍· (P , Ο† , i)
  Ξ³ = e , Ξ΄

\end{code}

Could the map (anti l m) be an equivalence? No. We instead have an
equivalence (l βŠ‘ m) Γ— (m βŠ‘ l) β†’ (l ＝ m) Γ— (l ＝ m), reflecting the
fact that there are two candidate proofs for the equality.

\begin{code}

to-⋍· : (l m : 𝓛 X) β†’ (l βŠ‘ m) Γ— (is-defined m β†’ is-defined l) β†’ (l ⋍· m)
to-⋍· (Q , ψ , j) (P , Ο† , i) ((f , Ξ΄) , g) =
  (f , ((g , (Ξ» p β†’ i (f (g p)) p)) , (g , (Ξ» q β†’ j (g (f q)) q)))) , Ξ΄

from-⋍· : (l m : 𝓛 X) β†’ (l ⋍· m) β†’ (l βŠ‘ m) Γ— (is-defined m β†’ is-defined l)
from-⋍· l m (f , g) = (⌜ f ⌝ , g) , ⌜ f ⌝⁻¹

from-to-⋍· : (l m : 𝓛 X) β†’  from-⋍· l m ∘ to-⋍· l m ∼ id
from-to-⋍· l m e = refl

to-from : funext 𝓣 𝓣 β†’ (l m : 𝓛 X) β†’ to-⋍· l m ∘ from-⋍· l m ∼ id
to-from fe l m 𝕗@((f , Ξ΄) , g) = b
 where
  Ξ΄' : is-equiv f
  Ξ΄' = ⌜ is-defined-⋍· l m (to-⋍· l m (from-⋍· l m 𝕗)) ⌝-is-equiv

  a : δ' ＝ δ
  a = being-equiv-is-prop'' fe f Ξ΄' Ξ΄

  b : (f , δ') , g ＝ (f , δ) , g
  b = ap (Ξ» - β†’ (f , -) , g) a

βŠ‘-anti-equiv-lemma'' : funext 𝓣 𝓣 β†’ (l m : 𝓛 X) β†’ is-equiv (to-⋍· l m)
βŠ‘-anti-equiv-lemma'' fe l m = qinvs-are-equivs
                               (to-⋍· l m)
                               (from-⋍· l m , from-to-⋍· l m , to-from fe l m)

βŠ‘-anti-equiv-lemma' : funext 𝓣 𝓣
                   β†’ (l m : 𝓛 X)
                   β†’ (l βŠ‘ m) Γ— (is-defined m β†’ is-defined l) ≃ (l ⋍· m)
βŠ‘-anti-equiv-lemma' fe l m = to-⋍· l m , βŠ‘-anti-equiv-lemma'' fe l m

βŠ‘-anti-equiv-lemma : is-univalent 𝓣
                   β†’ funext 𝓣 𝓀
                   β†’ (l m : 𝓛 X)
                   β†’ (l βŠ‘ m) Γ— (is-defined m β†’ is-defined l) ≃ (l ＝ m)
βŠ‘-anti-equiv-lemma ua fe l m =
  (βŠ‘-anti-equiv-lemma' (univalence-gives-funext ua) l m)
  ● (≃-sym (𝓛-IdΒ· ua fe l m))

βŠ‘-anti-equiv : is-univalent 𝓣
             β†’ funext 𝓣 𝓀
             β†’ (l m : 𝓛 X)
             β†’ (l βŠ‘ m) Γ— (m βŠ‘ l) ≃ (l ＝ m) Γ— (m ＝ l)
βŠ‘-anti-equiv ua fe l m = Ξ³ ● (Γ—-cong (βŠ‘-anti-equiv-lemma ua fe l m)
                                     (βŠ‘-anti-equiv-lemma ua fe m l))
 where
  A = (l βŠ‘ m) Γ— (m βŠ‘ l)

  B = ((l βŠ‘ m) Γ— (is-defined m β†’ is-defined l))
    Γ— ((m βŠ‘ l) Γ— (is-defined l β†’ is-defined m))

  Ξ³ : A ≃ B
  Ξ³ = qinveq u (v , vu , uv)
    where
     u : A β†’ B
     u ((f , Ξ΄) , (g , Ξ΅)) = ((f , Ξ΄) , g) , ((g , Ξ΅) , f)

     v : B β†’ A
     v (((f , Ξ΄) , h) , ((g , Ξ΅) , k)) = (f , Ξ΄) , (g , Ξ΅)

     vu : (a : A) β†’ v (u a) ＝ a
     vu a = refl

     uv : (b : B) β†’ u (v b) ＝ b
     uv (((f , Ξ΄) , h) , ((g , Ξ΅) , k)) = t
      where
       r : g ＝ h
       r = dfunext
            (univalence-gives-funext ua)
            (Ξ» p β†’ being-defined-is-prop l (g p) (h p))
       s : f ＝ k
       s = dfunext
            (univalence-gives-funext ua)
            (Ξ» p β†’ being-defined-is-prop m (f p) (k p))

       t : ((f , δ) , g) , (g , Ρ) , f ＝ ((f , δ) , h) , (g , Ρ) , k
       t = apβ‚‚ (Ξ» -β‚€ -₁ β†’ ((f , Ξ΄) , -β‚€) , (g , Ξ΅) , -₁) r s

\end{code}

Next we show that (l βŠ‘ m) ≃ (is-defined l β†’ l ＝ m), so that elements
of l βŠ‘ m can be seen as partial elements of the identity type l ＝ m.

We begin with the following auxiliary construction, which shows that
the type l βŠ‘ m is modal for the open modality induced by the
proposition "is-defined l" (and gave me a headache):

\begin{code}

βŠ‘-open : funext 𝓣 𝓣
       β†’ funext 𝓣 (𝓣 βŠ” 𝓀)
       β†’ (l m : 𝓛 X) β†’ (l βŠ‘ m) ≃ (is-defined l β†’ l βŠ‘ m)
βŠ‘-open fe fe'' (Q , ψ , j) (P , Ο† , i) = qinveq Ο€ (ρ , ρπ , πρ)
 where
  l = (Q , ψ , j)

  m = (P , Ο† , i)

  Ο€ : l βŠ‘ m β†’ (is-defined l β†’ l βŠ‘ m)
  Ο€ Ξ± d = Ξ±

  ρ : (is-defined l β†’ l βŠ‘ m) β†’ l βŠ‘ m
  ρ h = (Ξ» d β†’ def-pr l m (h d) d) , (Ξ» d β†’ val-pr l m (h d) d)

  ρπ : ρ ∘ Ο€ ∼ id
  ρπ Ξ± = refl

  ρ-lemma : (h : is-defined l β†’ l βŠ‘ m) (q : is-defined l) β†’ ρ h ＝ h q
  ρ-lemma h q = γ
   where
    remark : h q ＝ def-pr l m (h q) , val-pr l m (h q)
    remark = refl

    k : (d : Q) β†’ def-pr l m (h d) d ＝ def-pr l m (h q) d
    k d = ap (Ξ» - β†’ def-pr l m (h -) d) (j d q)

    a : (Ξ» d β†’ def-pr l m (h d) d) ＝ def-pr l m (h q)
    a = dfunext fe k

    u : (d : Q) {f g : Q β†’ P} (k : f ∼ g)
      β†’ ap (Ξ» (- : Q β†’ P) β†’ Ο† (- d)) (dfunext fe k) ＝ ap Ο† (k d)
    u d {f} {g} k = ap-funext f g Ο† k fe d

    v : (d : Q) β†’ val-pr l m (h d) d βˆ™ ap (Ξ» - β†’ Ο† (- d)) a
                ＝ val-pr l m (h q) d
    v d =
     val-pr l m (h d) d βˆ™ ap (Ξ» - β†’ Ο† (- d)) a                         ＝⟨ I ⟩
     val-pr l m (h d) d βˆ™ ap Ο† (ap (Ξ» - β†’ def-pr l m (h -) d) (j d q)) ＝⟨ II ⟩
     val-pr l m (h d) d βˆ™ ap (Ξ» - β†’ Ο† (def-pr l m (h -) d)) (j d q)    ＝⟨ III ⟩
     ap (Ξ» _ β†’ ψ d) (j d q) βˆ™ val-pr l m (h q) d                       ＝⟨ IV ⟩
     refl βˆ™ val-pr l m (h q) d                                         ＝⟨ V ⟩
     val-pr l m (h q) d                                                ∎
      where
       I   = ap (Ξ» - β†’ val-pr l m (h d) d βˆ™ -) (u d k)
       II  = ap (Ξ» - β†’ val-pr l m (h d) d βˆ™ -)
                (ap-ap (Ξ» - β†’ def-pr l m (h -) d) Ο† (j d q))
       III = homotopies-are-natural
              (Ξ» _ β†’ ψ d)
              (Ξ» - β†’ Ο† (def-pr l m (h -) d))
              (Ξ» - β†’ val-pr l m (h -) d)
              {d} {q} {j d q}
       IV  = ap (Ξ» - β†’ - βˆ™ val-pr l m (h q) d) (ap-const (ψ d) (j d q))
       V   = refl-left-neutral

    t : {f g : Q β†’ P} (r : f ＝ g) (h : ψ ∼ Ο† ∘ f)
      β†’ transport (Ξ» - β†’ ψ ∼ Ο† ∘ -) r h ＝ Ξ» q β†’ h q βˆ™ ap (Ξ» - β†’ Ο† (- q)) r
    t refl h = refl

    b = transport (Ξ» - β†’ ψ ∼ Ο† ∘ -) a (Ξ» d β†’ val-pr l m (h d) d) ＝⟨ I ⟩
        (Ξ» d β†’ val-pr l m (h d) d βˆ™ ap (Ξ» - β†’ Ο† (- d)) a)        ＝⟨ II ⟩
        val-pr l m (h q)                                         ∎
         where
          I  = t a (Ξ» d β†’ val-pr l m (h d) d)
          II = dfunext (lower-funext 𝓣 𝓣 fe'') v

    Ξ³ : (Ξ» d β†’ def-pr l m (h d) d) , (Ξ» d β†’ val-pr l m (h d) d) ＝ h q
    γ = to-Σ-＝ (a , b)

  πρ :  Ο€ ∘ ρ ∼ id
  πρ h = dfunext fe'' (ρ-lemma h)

\end{code}

Using this we have the following, as promised:

\begin{code}

βŠ‘-in-terms-of-＝ : is-univalent 𝓣
                β†’ funext 𝓣 (𝓣 ⁺ βŠ” 𝓀)
                β†’ (l m : 𝓛 X) β†’ (l βŠ‘ m) ≃ (is-defined l β†’ l ＝ m)
βŠ‘-in-terms-of-＝ ua fe⁺ l m =
 l βŠ‘ m                                                                 β‰ƒβŸ¨ a ⟩
 (is-defined l β†’ l βŠ‘ m)                                                β‰ƒβŸ¨ b ⟩
 ((is-defined l β†’ l βŠ‘ m) Γ— πŸ™)                                          β‰ƒβŸ¨ c ⟩
 (is-defined l β†’ l βŠ‘ m) Γ— (is-defined l β†’ is-defined m β†’ is-defined l) β‰ƒβŸ¨ d ⟩
 (is-defined l β†’ (l βŠ‘ m) Γ— (is-defined m β†’ is-defined l))              β‰ƒβŸ¨ e ⟩
 (is-defined l β†’ l ＝ m)                                                β– 
 where
  fe : funext 𝓣 𝓣
  fe = univalence-gives-funext ua
  s : (is-defined l β†’ is-defined m β†’ is-defined l) ≃ πŸ™ {𝓀}
  s = singleton-≃-πŸ™
       ((Ξ» d e β†’ d) ,
        Ξ -is-prop fe
          (Ξ» d β†’ Ξ -is-prop fe
                   (Ξ» e β†’ being-defined-is-prop l)) (Ξ» d e β†’ d))

  a = βŠ‘-open fe (lower-funext 𝓣 ((𝓣 ⁺) βŠ” 𝓀) fe⁺) l m
  b =  ≃-sym πŸ™-rneutral
  c = Γ—-cong (≃-refl _) (≃-sym s)
  d = ≃-sym Ξ Ξ£-distr-≃
  e = β†’cong fe⁺
       (lower-funext 𝓣 ((𝓣 ⁺) βŠ” 𝓀) fe⁺)
       (≃-refl (is-defined l))
       (βŠ‘-anti-equiv-lemma ua (lower-funext 𝓣 ((𝓣 ⁺) βŠ” 𝓀) fe⁺) l m)

\end{code}

And we also get the promised map l βŠ‘ m β†’ 𝓛 (l ＝ m) that regards
elements of hom-type l βŠ‘ m as partial element of identity the type l ＝ m.
(Conjectural conjecture: this map is an embedding.)

TODO. This map should be an embedding.

\begin{code}

βŠ‘-lift : is-univalent 𝓣
       β†’ funext 𝓣 (𝓣 ⁺ βŠ” 𝓀)
       β†’ (l m : 𝓛 X) β†’ l βŠ‘ m β†’ 𝓛 (l ＝ m)
βŠ‘-lift ua fe l m Ξ± = is-defined l ,
                     ⌜ βŠ‘-in-terms-of-＝ ua fe l m ⌝ Ξ± ,
                     being-defined-is-prop l
\end{code}

We now show that the pre-∞-category 𝓛 X is univalent if the universe 𝓣
is univalent and we have enough function extensionality for 𝓣 and 𝓀.

\begin{code}

𝓛-pre-comp-with : (l m : 𝓛 X) β†’ l βŠ‘ m β†’ (n : 𝓛 X) β†’ m βŠ‘ n β†’ l βŠ‘ n
𝓛-pre-comp-with l m Ξ± n = 𝓛-comp l m n Ξ±

is-𝓛-equiv : (l m : 𝓛 X) β†’ l βŠ‘ m β†’ 𝓣 ⁺ βŠ” 𝓀 Μ‡
is-𝓛-equiv l m Ξ± = (n : 𝓛 X) β†’ is-equiv (𝓛-pre-comp-with l m Ξ± n)

being-𝓛-equiv-is-prop : funext (𝓣 ⁺ βŠ” 𝓀) (𝓣 βŠ” 𝓀)
                      β†’ (l m : 𝓛 X) (Ξ± : l βŠ‘ m)
                      β†’ is-prop (is-𝓛-equiv l m Ξ±)
being-𝓛-equiv-is-prop fe l m Ξ± =
 Ξ -is-prop fe
  (Ξ» n β†’ being-equiv-is-prop''
          (lower-funext (𝓣 ⁺) 𝓀 fe)
          (𝓛-pre-comp-with l m Ξ± n))

is-𝓛-equivβ†’ : (l m : 𝓛 X) (Ξ± : l βŠ‘ m)
            β†’ is-𝓛-equiv l m Ξ±
            β†’ is-equiv (def-pr l m Ξ±)
is-𝓛-equivβ†’ l m Ξ± e =
 qinvs-are-equivs
  (def-pr l m Ξ±)
  (def-pr m l Ξ² ,
    (Ξ» p β†’ being-defined-is-prop l
            (def-pr m l Ξ²
              (def-pr l m Ξ± p)) p) ,
    (Ξ» q β†’ being-defined-is-prop m
            (def-pr l m Ξ±
              (def-pr m l Ξ² q)) q))
 where
  u : m βŠ‘ l β†’ l βŠ‘ l
  u = 𝓛-pre-comp-with l m Ξ± l

  Ξ² : m βŠ‘ l
  Ξ² = inverse u (e l) (𝓛-id l)

is-𝓛-equiv← : propext 𝓣
            β†’ funext 𝓣 𝓣
            β†’ funext 𝓣 𝓀
            β†’ (l m : 𝓛 X) (Ξ± : l βŠ‘ m)
            β†’ is-equiv (def-pr l m Ξ±)
            β†’ is-𝓛-equiv l m Ξ±
is-𝓛-equiv← pe fe fe' l m Ξ± e = Ξ³
 where
  r : l ＝ m
  r = βŠ‘-anti-lemma pe fe fe' Ξ± (inverse (def-pr l m Ξ±) e)

  Ο€ : (l n : 𝓛 X) (Ξ± : l βŠ‘ l)
    β†’ def-pr l l Ξ± ＝ id
    β†’ Ξ£ Ξ΄ κž‰ ((q : is-defined l) β†’ value l q ＝ value l q)
          , 𝓛-pre-comp-with l l Ξ± n
            ∼ Ξ» Ξ² β†’ (def-pr l n Ξ² , (Ξ» q β†’ Ξ΄ q βˆ™ val-pr l n Ξ² q))
  Ο€ l n (.id , Ξ΄) refl = Ξ΄ , Ξ» Ξ² β†’ refl

  ρ : (l : 𝓛 X) (Ξ± : l βŠ‘ l)
    β†’ is-equiv (def-pr l l Ξ±)
    β†’ is-𝓛-equiv l l Ξ±
  ρ l Ξ± e n = equiv-closed-under-∼ u (𝓛-pre-comp-with l l Ξ± n) i h
   where
    s : def-pr l l α ＝ id
    s = dfunext fe (Ξ» q β†’ being-defined-is-prop l
                           (def-pr l l Ξ± q) q)

    Ξ΄ : (q : is-defined l) β†’ value l q ＝ value l q
    Ξ΄ = pr₁ (Ο€ l n Ξ± s)

    u : l βŠ‘ n β†’ l βŠ‘ n
    u Ξ² = def-pr l n Ξ² , Ξ» q β†’ Ξ΄ q βˆ™ val-pr l n Ξ² q

    h : 𝓛-pre-comp-with l l Ξ± n ∼ u
    h = prβ‚‚ (Ο€ l n Ξ± s)

    v : l βŠ‘ n β†’ l βŠ‘ n
    v Ξ³ = def-pr l n Ξ³ ,
          (Ξ» p β†’ (Ξ΄ p)⁻¹ βˆ™ val-pr l n Ξ³ p)

    vu : v ∘ u ∼ id
    vu (g , Ρ) = to-Σ-＝ (refl , dfunext fe' a)
     where
      a : (q : is-defined l) β†’ (Ξ΄ q)⁻¹ βˆ™ (Ξ΄ q βˆ™ Ξ΅ q) ＝ Ξ΅ q
      a q = (Ξ΄ q)⁻¹ βˆ™ (Ξ΄ q βˆ™ Ξ΅ q) ＝⟨ I ⟩
            ((Ξ΄ q)⁻¹ βˆ™ Ξ΄ q) βˆ™ Ξ΅ q ＝⟨ II ⟩
            refl βˆ™ Ξ΅ q            ＝⟨ III ⟩
            Ρ q                   ∎
             where
              I   = (βˆ™assoc ((Ξ΄ q)⁻¹) (Ξ΄ q) (Ξ΅ q))⁻¹
              II  = ap (Ξ» - β†’ - βˆ™ Ξ΅ q) ((sym-is-inverse (Ξ΄ q))⁻¹)
              III = refl-left-neutral

    uv : u ∘ v ∼ id
    uv (g , Ρ) = to-Σ-＝ (refl , dfunext fe' a)
     where
      a : (q : is-defined l) β†’ Ξ΄ q βˆ™ ((Ξ΄ q)⁻¹ βˆ™ Ξ΅ q) ＝ Ξ΅ q
      a q = Ξ΄ q βˆ™ ((Ξ΄ q)⁻¹ βˆ™ Ξ΅ q)  ＝⟨ I ⟩
           (Ξ΄ q βˆ™ ((Ξ΄ q)⁻¹)) βˆ™ Ξ΅ q ＝⟨ II ⟩
            refl βˆ™ Ξ΅ q             ＝⟨ III ⟩
            Ρ q                    ∎
             where
              I   = (βˆ™assoc (Ξ΄ q) ((Ξ΄ q)⁻¹) (Ξ΅ q))⁻¹
              II  = ap (Ξ» - β†’ - βˆ™ Ξ΅ q) ((sym-is-inverse' (Ξ΄ q))⁻¹)
              III = refl-left-neutral

    i : is-equiv u
    i = qinvs-are-equivs u (v , vu , uv)

  Οƒ : (l m : 𝓛 X)
    β†’ l ＝ m
    β†’ (Ξ± : l βŠ‘ m)
    β†’ is-equiv (def-pr l m Ξ±)
    β†’ is-𝓛-equiv l m Ξ±
  Οƒ l .l refl = ρ l

  Ξ³ : is-𝓛-equiv l m Ξ±
  Ξ³ = Οƒ l m r Ξ± e

\end{code}

With this and Yoneda we can now easily derive the univalence of the
pre-∞-category 𝓛 X.

The univalence of 𝓣 is more than we need in the
following. Propositional extensionality for propositions in 𝓣
suffices, but the way we proved this using a general SIP relies on
univalence (we could prove a specialized version of the SIP, but this
is probably not worth the trouble (we'll see)).

\begin{code}

module univalence-of-𝓛 (ua : is-univalent 𝓣)
                       (fe : Fun-Ext)
       where

 pe : propext 𝓣
 pe = univalence-gives-propext ua

 is-𝓛-equiv-charac : (l m : 𝓛 X) (Ξ± : l βŠ‘ m)
                   β†’ is-𝓛-equiv l m Ξ± ≃ (is-defined m β†’ is-defined l)
 is-𝓛-equiv-charac l m Ξ± =
  is-𝓛-equiv l m Ξ±              β‰ƒβŸ¨ a ⟩
  is-equiv (def-pr l m Ξ±)   β‰ƒβŸ¨ b ⟩
  (is-defined m β†’ is-defined l) β– 
  where
   a = logically-equivalent-props-are-equivalent
        (being-𝓛-equiv-is-prop fe l m Ξ±)
        (being-equiv-is-prop'' fe (def-pr l m Ξ±))
        (is-𝓛-equivβ†’ l m Ξ±)
        (is-𝓛-equiv← pe fe fe l m Ξ±)

   b = logically-equivalent-props-are-equivalent
        (being-equiv-is-prop'' fe (def-pr l m Ξ±))
        (Ξ -is-prop fe (Ξ» p β†’ being-defined-is-prop l))
        (inverse (def-pr l m Ξ±))
        (Ξ» g β†’ qinvs-are-equivs
                (def-pr l m Ξ±)
                (g ,
                 (Ξ» q β†’ being-defined-is-prop l
                         (g (def-pr l m Ξ± q)) q) ,
                 (Ξ» p β†’ being-defined-is-prop m
                         (def-pr l m Ξ± (g p)) p)))

 _β‰ƒβŸ¨π“›βŸ©_ : 𝓛 X β†’ 𝓛 X β†’ 𝓣 ⁺ βŠ” 𝓀 Μ‡
 l β‰ƒβŸ¨π“›βŸ© m = Ξ£ Ξ± κž‰ l βŠ‘ m , is-𝓛-equiv l m Ξ±

 β‰ƒβŸ¨π“›βŸ©-charac : (l m : 𝓛 X)
             β†’ (l β‰ƒβŸ¨π“›βŸ© m) ≃ (l βŠ‘ m) Γ— (is-defined m β†’ is-defined l)
 β‰ƒβŸ¨π“›βŸ©-charac l m = Ξ£-cong (is-𝓛-equiv-charac l m)

 β‰ƒβŸ¨π“›βŸ©-is-Id : (l m : 𝓛 X)
            β†’ (l β‰ƒβŸ¨π“›βŸ© m) ≃ (l ＝ m)
 β‰ƒβŸ¨π“›βŸ©-is-Id l m = (β‰ƒβŸ¨π“›βŸ©-charac l m) ● (βŠ‘-anti-equiv-lemma ua fe l m)

 𝓛-is-univalent' : (l : 𝓛 X) β†’ βˆƒ! m κž‰ 𝓛 X , (l β‰ƒβŸ¨π“›βŸ© m)
 𝓛-is-univalent' l = equiv-to-singleton e (singleton-types-are-singletons l)
  where
    e : (Ξ£ m κž‰ 𝓛 X , l β‰ƒβŸ¨π“›βŸ© m) ≃ (Ξ£ m κž‰ 𝓛 X , l ＝ m)
    e = Ξ£-cong (β‰ƒβŸ¨π“›βŸ©-is-Id l)

 𝓛-id-is-𝓛-equiv : (l : 𝓛 X) β†’ is-𝓛-equiv l l (𝓛-id l)
 𝓛-id-is-𝓛-equiv l n = (id , h) , (id , h)
  where
   h : 𝓛-pre-comp-with l l (𝓛-id l) n ∼ id
   h (f , Ξ΄) = to-Ξ£-＝ (refl , dfunext fe (Ξ» p β†’ refl-left-neutral))

 𝓛-refl : (l : 𝓛 X) β†’ l β‰ƒβŸ¨π“›βŸ© l
 𝓛-refl l = 𝓛-id l , 𝓛-id-is-𝓛-equiv l

 Id-to-𝓛-eq : (l m : 𝓛 X) β†’ l ＝ m β†’ l β‰ƒβŸ¨π“›βŸ© m
 Id-to-𝓛-eq l m r = transport (l β‰ƒβŸ¨π“›βŸ©_) r (𝓛-refl l)

 𝓛-is-univalent : (l m : 𝓛 X) β†’ is-equiv (Id-to-𝓛-eq l m)
 𝓛-is-univalent l = universality-equiv l (𝓛-refl l)
                     (central-point-is-universal (l β‰ƒβŸ¨π“›βŸ©_) (l , 𝓛-refl l)
                       (singletons-are-props (𝓛-is-univalent' l) (l , 𝓛-refl l)))
  where
   open import UF.Yoneda

 \end{code}

This completes the main goal of the module.

We have yet another equivalence, using the above techniques:

\begin{code}

Ξ·-maximal' : (x : X) (l : 𝓛 X) β†’ Ξ· x βŠ‘ l β†’ l βŠ‘ Ξ· x
Ξ·-maximal' x (P , ψ , i) (f , Ξ΄) = (Ξ» p β†’ ⋆) , (Ξ» p β†’ ap ψ (i p (f ⋆)) βˆ™ (Ξ΄ ⋆)⁻¹)

Ξ·-maximal : propext 𝓣
          β†’ funext 𝓣 𝓣
          β†’ funext 𝓣 𝓀
          β†’ (x : X) (l : 𝓛 X)
          β†’ Ξ· x βŠ‘ l
          β†’ Ξ· x ＝ l
Ξ·-maximal pe fe fe' x l a = βŠ‘-anti pe fe fe' (a , Ξ·-maximal' x l a)

βŠ₯-least : (l : 𝓛 X) β†’ βŠ₯ βŠ‘ l
βŠ₯-least l = unique-from-𝟘 , Ξ» z β†’ unique-from-𝟘 z

βŠ₯-initial : funext 𝓣 𝓣
          β†’ funext 𝓣 𝓀
          β†’ (l : 𝓛 X) β†’ is-singleton (βŠ₯ βŠ‘ l)
βŠ₯-initial fe fe' l = βŠ₯-least l ,
                     (Ξ» Ξ± β†’ to-Ξ£-＝ (dfunext fe (Ξ» z β†’ unique-from-𝟘 z) ,
                                     dfunext fe'(Ξ» z β†’ unique-from-𝟘 z)))

Ξ·-＝-gives-βŠ‘ : {x y : X} β†’ x ＝ y β†’ Ξ· x βŠ‘ Ξ· y
Ξ·-＝-gives-βŠ‘ {x} {y} p = id , (Ξ» d β†’ p)

Ξ·-βŠ‘-gives-＝ : {x y : X} β†’ Ξ· x βŠ‘ Ξ· y β†’ x ＝ y
Ξ·-βŠ‘-gives-＝ (f , Ξ΄) = Ξ΄ ⋆

Ξ·-＝-gives-βŠ‘-is-equiv : funext 𝓣 𝓣
                     β†’ funext 𝓣 𝓀
                     β†’ {x y : X} β†’ is-equiv (Ξ·-＝-gives-βŠ‘ {x} {y})
Ξ·-＝-gives-βŠ‘-is-equiv fe fe' {x} {y} =
 qinvs-are-equivs Ξ·-＝-gives-βŠ‘ (Ξ·-βŠ‘-gives-＝ , Ξ± , Ξ²)
 where
  Ξ± : {x y : X} (p : x ＝ y) β†’  Ξ·-βŠ‘-gives-＝ (Ξ·-＝-gives-βŠ‘ p) ＝ p
  Ξ± p = refl

  Ξ² : {x y : X} (q : Ξ· x βŠ‘ Ξ· y) β†’ Ξ·-＝-gives-βŠ‘ (Ξ·-βŠ‘-gives-＝ q) ＝ q
  Ξ² (f , Ξ΄) = to-Γ—-＝
               (dfunext fe (Ξ» x β†’ πŸ™-is-prop x (f x)))
               (dfunext fe' (Ξ» x β†’ ap Ξ΄ (πŸ™-is-prop ⋆ x)))

Id-via-lifting : funext 𝓣 𝓣
               β†’ funext 𝓣 𝓀
               β†’ {x y : X} β†’ (x ＝ y) ≃ (Ξ· x βŠ‘ Ξ· y)
Id-via-lifting fe fe' = Ξ·-＝-gives-βŠ‘ , Ξ·-＝-gives-βŠ‘-is-equiv fe fe'

\end{code}

Added 13th March 2024.

\begin{code}

Ξ·-image : funext 𝓣 𝓣
        β†’ funext 𝓣 𝓀
        β†’ propext 𝓣
        β†’ {X : 𝓀 Μ‡ }
        β†’ Β¬ (Ξ£ l κž‰ 𝓛 X , (l β‰  βŠ₯) Γ— ((x : X) β†’ l β‰  Ξ· x))
Ξ·-image fe fe' pe ((P , Ο† , P-is-prop) , Ξ½ , f) =
 no-props-other-than-𝟘-or-πŸ™ pe (P , P-is-prop , g , h)
 where
  g : ¬ (P ＝ 𝟘)
  g e = ν (to-Σ-＝
            (e ,
             to-subtype-＝
              (Ξ» _ β†’ being-prop-is-prop fe)
              (dfunext fe' (Ξ» x β†’ 𝟘-elim x))))

  h : Β¬ (P ＝ πŸ™)
  h refl = f (Ο† ⋆)
             (to-Σ-＝
               (refl ,
                to-subtype-＝
                 (Ξ» _ β†’ being-prop-is-prop fe)
                 (dfunext fe' (Ξ» ⋆ β†’ refl))))

Ξ·-bounded : (y : 𝓛 X) (x x' : X) β†’ Ξ· x βŠ‘ y β†’ Ξ· x' βŠ‘ y β†’ x ＝ x'
Ξ·-bounded y@(P , Ο† , P-is-prop) x x' (p , e) (p' , e') =
 x        ＝⟨ e ⋆ ⟩
 Ο† (p  ⋆) ＝⟨ ap Ο† (P-is-prop (p ⋆) (p' ⋆)) ⟩
 Ο† (p' ⋆) ＝⟨ (e' ⋆)⁻¹ ⟩
 x'       ∎

\end{code}