Martin Escardo. 19th December 2020, June 2023.

General properties of W-types.

Notice that we don't assume any axioms from univalent foundations
other than function extensionality, but that we formulate and prove
properties in univalent style.

\begin{code}

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

open import MLTT.Spartan

module W.Properties (X : 𝓤 ̇ ) (A : X → 𝓥 ̇ ) where

open import UF.Base
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.FunExt
open import UF.Retracts
open import UF.Sets
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import W.Type

private
 𝕎 = W X A

\end{code}

We first show that the identity type of 𝕎 is equivalent to _＝ʷ_
defined as follows.

\begin{code}

_＝ʷ_ : 𝕎 → 𝕎 → 𝓤 ⊔ 𝓥 ̇
ssup x f ＝ʷ ssup x' f' = Σ p ꞉ x ＝ x' , ((a : A x) → f a ＝ʷ f' (transport A p a))

＝ʷ-refl : (w : 𝕎) → w ＝ʷ w
＝ʷ-refl (ssup x f) = refl , (λ a → ＝ʷ-refl (f a))

singleton-typeʷ : 𝕎 → 𝓤 ⊔ 𝓥 ̇
singleton-typeʷ w = Σ t ꞉ 𝕎 , w ＝ʷ t

W-center : (w : 𝕎) → singleton-typeʷ w
W-center w = w , ＝ʷ-refl w

W-centrality : Fun-Ext → (w : 𝕎) (σ : singleton-typeʷ w) → W-center w ＝ σ
W-centrality fe w@(ssup x f) σ@(ssup x g , refl , u) = IV
 where
  have-u : (a : A x) → f a ＝ʷ g a
  have-u = u

  IH : (a : A x) → W-center (f a) ＝ (g a , u a)
  IH a = W-centrality fe (f a) (g a , u a)

  I : (λ a → W-center (f a)) ＝ (λ a → g a , u a)
  I = dfunext fe IH

  π : (Σ h ꞉ (A x → 𝕎) , ((a : A x) → f a ＝ʷ h a))
    → singleton-typeʷ (ssup x f)
  π (h , v) = ssup x h , refl , v

  II : (f , λ a → ＝ʷ-refl (f a)) ＝[ domain π ] (g , u)
  II = ap ΠΣ-distr I

  III : (ssup x f , refl , (λ a → ＝ʷ-refl (f a))) ＝ (ssup x g , refl , u)
  III = ap π II

  IV = W-center w                               ＝⟨ refl ⟩
       ssup x f , refl , (λ a → ＝ʷ-refl (f a)) ＝⟨ III ⟩
       ssup x g , refl , u                      ＝⟨ refl ⟩
       σ                                        ∎

singleton-typesʷ-are-singletons : Fun-Ext
                                → (w : 𝕎) → is-singleton (singleton-typeʷ w)
singleton-typesʷ-are-singletons fe w = W-center w , W-centrality fe w

\end{code}

From this it follows that the canonical map from the native notion of
𝕎-identity to the alternative notion of 𝕎-identity defined above is an
equivalence:

\begin{code}

idtoidʷ : (w t : 𝕎) → w ＝ t → w ＝ʷ t
idtoidʷ w w refl = ＝ʷ-refl w

idtoidʷ-is-equiv : Fun-Ext → (w t : 𝕎) → is-equiv (idtoidʷ w t)
idtoidʷ-is-equiv fe w = I
 where
  f : singleton-type w → singleton-typeʷ w
  f = NatΣ (idtoidʷ w)

  f-is-equiv : is-equiv f
  f-is-equiv = maps-of-singletons-are-equivs f
                (singleton-types-are-singletons w)
                (singleton-typesʷ-are-singletons fe w)

  I : (t : 𝕎) → is-equiv (idtoidʷ w t)
  I = NatΣ-equiv-gives-fiberwise-equiv (idtoidʷ w) f-is-equiv

idtoidʷ-≃ : Fun-Ext → (w t : 𝕎) → (w ＝ t) ≃ (w ＝ʷ t)
idtoidʷ-≃ fe w t = idtoidʷ w t , idtoidʷ-is-equiv fe w t

\end{code}

We now describe ways to "construct" and "destruct" native 𝕎
identifications, which are mutually inverse and hence induce an
equivalence.

\begin{code}

to-W-＝ : {x  : X} {φ  : A x  → 𝕎}
          {x' : X} {φ' : A x' → 𝕎}
        → (Σ p ꞉ x ＝ x' , (φ ＝ φ' ∘ transport A p))
        → ssup x φ ＝[ 𝕎 ] ssup x' φ'
to-W-＝ {x} {φ} {x} {φ'} (refl , f) = ap (ssup x) f

from-W-＝ : {x  : X} {φ  : A x  → 𝕎}
              {x' : X} {φ' : A x' → 𝕎}
            → ssup x φ ＝[ 𝕎 ] ssup x' φ'
            → (Σ p ꞉ x ＝ x' , (φ ＝ φ' ∘ transport A p))
from-W-＝ refl = refl , refl

to-from-W-＝ : {x  : X} {φ  : A x  → 𝕎}
               {x' : X} {φ' : A x' → 𝕎}
            → (q : ssup x φ ＝[ 𝕎 ] ssup x' φ')
            → to-W-＝ (from-W-＝ q) ＝ q
to-from-W-＝ refl = refl

from-to-W-＝ : {x  : X} {φ  : A x  → 𝕎}
               {x' : X} {φ' : A x' → 𝕎}
            → (σ : Σ p ꞉ x ＝ x' , (φ ＝ φ' ∘ transport A p))
            → from-W-＝ (to-W-＝ {x} {φ} {x'} {φ'} σ) ＝  σ
from-to-W-＝ (refl , refl) = refl

W-＝ : {x  : X} {φ  : A x  → 𝕎}
       {x' : X} {φ' : A x' → 𝕎}
     → (ssup x φ ＝[ 𝕎 ] ssup x' φ')
     ≃ (Σ p ꞉ x ＝ x' , (φ ＝ φ' ∘ transport A p))
W-＝ {x} {φ} {x'} {φ'} = qinveq
                          from-W-＝
                          (to-W-＝ ,
                           to-from-W-＝ ,
                           from-to-W-＝ {x} {φ} {x'} {φ'})
\end{code}

From this we conclude that if X is a proposition or a set, then 𝕎 is a
proposition or a set respectively:

\begin{code}

W-is-prop : funext 𝓥 (𝓤 ⊔ 𝓥)
          → is-prop X
          → is-prop 𝕎
W-is-prop fe X-is-prop (ssup x φ) (ssup x' φ') = γ
 where
  p : x ＝ x'
  p = X-is-prop x x'

  IH : (a : A x) → φ a ＝ φ' (transport A p a)
  IH a = W-is-prop fe X-is-prop (φ a) (φ' (transport A p a))

  γ : ssup x φ ＝ ssup x' φ'
  γ = to-W-＝ (p , dfunext fe IH)

W-is-set : funext 𝓥 (𝓤 ⊔ 𝓥)
         → is-set X
         → is-set 𝕎
W-is-set fe X-is-set {ssup x φ} {ssup x' φ'} = γ
 where
  S = Σ p ꞉ x ＝ x' , (φ ∼ φ' ∘ transport A p)

  IH : (p : x ＝ x') (a : A x) → is-prop (φ a ＝ φ' (transport A p a))
  IH p a = W-is-set fe X-is-set {φ a} {φ' (transport A p a)}

  α : is-prop S
  α = Σ-is-prop X-is-set (λ p → Π-is-prop fe (IH p))

  β : retract (ssup x φ ＝ ssup x' φ') of S
  β = (λ (p , h) → to-W-＝ (p , dfunext fe h)) ,
      (λ p → pr₁ (from-W-＝ p) , happly (pr₂ (from-W-＝ p))) ,
      h
    where
     h : (λ (p : ssup x (λ v → φ v) ＝ ssup x' (λ v → φ' v))
         → to-W-＝ (pr₁ (from-W-＝ p) , dfunext fe (happly (pr₂ (from-W-＝ p)))))
       ∼ id
     h refl =  ap (ssup x) (dfunext fe (happly refl)) ＝⟨ I ⟩
               ap (ssup x) refl                       ＝⟨ refl ⟩
               refl                                   ∎
                where
                 I = ap (ap (ssup x)) (funext-happly fe φ φ refl)

  γ : is-prop (ssup x φ ＝ ssup x' φ')
  γ = retract-of-prop β α

\end{code}

Notice that, in both cases, we didn't need to assume anything about
the family A to deduce the truncation level of the type 𝕎 = W X A.
Only the truncation level of X matters.