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.


{-# 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

 𝕎 = W X A


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


_=ʷ_ : 𝕎  𝕎  𝓤  𝓥 ̇
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
  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


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


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


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


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
                          (to-W-= ,
                           to-from-W-= ,
                           from-to-W-= {x} {φ} {x'} {φ'})

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


W-is-prop : funext 𝓥 (𝓤  𝓥)
           is-prop X
           is-prop 𝕎
W-is-prop fe X-is-prop (ssup x φ) (ssup x' φ') = γ
  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' φ'} = γ
  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 :  (p : ssup x  v  φ v)  ssup x'  v  φ' v))
          to-W-= (pr₁ (from-W-= p) , dfunext fe (happly (pr₂ (from-W-= p)))))
     h refl =  ap (ssup x) (dfunext fe (happly refl)) =⟨ I 
               ap (ssup x) refl                       =⟨ refl 
                 I = ap (ap (ssup x)) (funext-happly fe φ φ refl)

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


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.