Lifting.UnivalentWildCategory

Martin Escardo December 2018.

The lifting of a type forms a univalent wild-∞-category with hom types
l ⊑ m, which is a partial order if the type is a set (wild because we
are not giving coherence data).



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

open import MLTT.Spartan

module Lifting.UnivalentWildCategory
        (𝓣 : 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


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!).


_⊑_ : 𝓛 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)))))


Thus, the associativity law in this wild-∞-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 wild-∞-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:


⊑-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) _ ε)


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.


⊑-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


We can now establish the promised fact:


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


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:


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


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:


⊑-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 , δ


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.


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


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):


⊑-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)


Using this we have the following, as promised:


⊑-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)


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.


⊑-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

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


𝓛-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


With this and Yoneda we can now easily derive the univalence of the
wild-∞-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)).


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


This completes the main goal of the module.

We have yet another equivalence, using the above techniques:


η-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'


Added 13th March 2024.


η-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'       ∎


TODO. Monad algebras should also be univalent wild-∞-categories.