Properties

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

private
 π•Ž = 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
 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


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:


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


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

We first do this for arbitrary elements of π•Ž, using the accessors
W-root and W-forest, and then get the case of elements given by ssup as
an instance.


W-Code : π•Ž β†’ π•Ž β†’ 𝓀 βŠ” π“₯ Μ‡
W-Code w t = Ξ£ p κž‰ W-root w ＝ W-root t
                 , (W-forest w ＝ W-forest t ∘ transport A p)

W-code : (w t : π•Ž) β†’ w ＝ t β†’ W-Code w t
W-code w _ refl = refl , refl

W-decode : (w t : π•Ž) β†’ W-Code w t β†’ w ＝ t
W-decode (ssup x Ο†) (ssup x' Ο†') (refl , f) = ap (ssup x) f

W-decode-code : (w t : π•Ž) (q : w ＝ t)
              β†’ W-decode w t (W-code w t q) ＝ q
W-decode-code (ssup x Ο†) _ refl = refl

to-W-＝ : {x  : X} {Ο†  : A x  β†’ π•Ž}
          {x' : X} {Ο†' : A x' β†’ π•Ž}
        β†’ (Ξ£ p κž‰ x ＝ x' , (Ο† ＝ Ο†' ∘ transport A p))
        β†’ ssup x Ο† ＝[ π•Ž ] ssup x' Ο†'
to-W-＝ {x} {Ο†} {x'} {Ο†'} = W-decode (ssup x Ο†) (ssup x' Ο†')

from-W-＝ : {x  : X} {Ο†  : A x  β†’ π•Ž}
              {x' : X} {Ο†' : A x' β†’ π•Ž}
            β†’ ssup x Ο† ＝[ π•Ž ] ssup x' Ο†'
            β†’ (Ξ£ p κž‰ x ＝ x' , (Ο† ＝ Ο†' ∘ transport A p))
from-W-＝ {x} {Ο†} {x'} {Ο†'} = W-code (ssup x Ο†) (ssup x' Ο†')

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-＝ {x} {Ο†} {x'} {Ο†'} = W-decode-code (ssup x Ο†) (ssup x' Ο†')

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'} {Ο†'})

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' Ο†') = Ξ³
 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 = k (ssup x' Ο†')
      where
       k : (t : π•Ž) (p : ssup x Ο† ＝ t)
         β†’ W-decode (ssup x Ο†) t
            (pr₁ (W-code (ssup x Ο†) t p) ,
             dfunext fe (happly (prβ‚‚ (W-code (ssup x Ο†) t p))))
         ＝ p
       k _ 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 Ξ² Ξ±


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.

When the two roots are literally the same, and X is a set, the
identification of the forests is a homotopy, the loop that from-W-＝
produces being refl and its transport therefore the identity.


forest-＝ : is-set X
         β†’ {x : X} {Ο† Ο†' : A x β†’ π•Ž}
         β†’ ssup x Ο† ＝ ssup x Ο†'
         β†’ Ο† ∼ Ο†'
forest-＝ X-is-set {x} {Ο†} {Ο†'} p = happly III
 where
  I : x ＝ x
  I = pr₁ (from-W-＝ p)

  II : Ο† ＝ Ο†' ∘ transport A I
  II = prβ‚‚ (from-W-＝ p)

  III : Ο† ＝ Ο†'
  III = transport (Ξ» - β†’ Ο† ＝ Ο†' ∘ transport A -) (X-is-set I refl) II