Martin Escardo, June 2023.

Paths in W-types.

\begin{code}

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

open import MLTT.Spartan

module W.Paths where

open import UF.Logic
open import UF.PropTrunc
open import UF.Subsingletons
open import W.Type
open import W.Numbers

module _ (X : 𝓀 Μ‡ ) (A : X β†’ π“₯ Μ‡ ) where

 private
  π•Ž = W X A

\end{code}

Paths whose lengths can be measured with natural numbers.

\begin{code}

 Pathβ‚€ : π•Ž β†’ 𝓀 βŠ” π“₯ Μ‡
 Pathβ‚€ (ssup x Ο†) = is-empty (A x) + (Ξ£ a κž‰ A x , Pathβ‚€ (Ο† a))

 Pathβ‚€-length : (w : π•Ž) β†’ Pathβ‚€ w β†’ β„•
 Pathβ‚€-length (ssup x Ο†) (inl _)        = 0
 Pathβ‚€-length (ssup x Ο†) (inr (a , as)) = succ (Pathβ‚€-length (Ο† a) as)

\end{code}

To construct such paths, we need to be able to decide pointedness. A
weaker notion that doesn't require this is the following.

\begin{code}

 module weaker-notion-of-path
         (pt : propositional-truncations-exist)
        where

  open PropositionalTruncation pt
  open Truncation pt renaming (βˆ₯_βˆ₯Ξ© to ⟦_⟧)

  Path : π•Ž β†’ 𝓀 βŠ” π“₯ Μ‡
  Path (ssup x Ο†) = βˆ₯ A x βˆ₯ β†’ Ξ£ a κž‰ A x , Path (Ο† a)

  head : {w : π•Ž} β†’ βˆ₯ A (W-root w) βˆ₯ β†’ Path w β†’ A (W-root w)
  head {ssup x Ο†} s as = pr₁ (as s)

  tail : {w : π•Ž} (s : βˆ₯ A (W-root w) βˆ₯) (as : Path w) β†’ Path (W-forest w (head s as))
  tail {ssup x Ο†} s as = prβ‚‚ (as s)

  Pathβ‚€-gives-Path : (w : π•Ž) β†’ Pathβ‚€ w β†’ Path w
  Pathβ‚€-gives-Path (ssup x Ο†) (inl e)         aβ‚€ = 𝟘-elim (βˆ₯βˆ₯-rec 𝟘-is-prop e aβ‚€)
  Pathβ‚€-gives-Path (ssup x Ο†) (inr (a , as))  aβ‚€ = a , Pathβ‚€-gives-Path (Ο† a) as

\end{code}

To measure the length of a path in the weaker sense, we need
generalized natural numbers.

\begin{code}

  Path-length : (w : π•Ž) β†’ Path w β†’ 𝓝
  Path-length (ssup x Ο†) as = Suc ⟦ A x ⟧
                               (Ξ» (s : βˆ₯ A x βˆ₯) β†’ Path-length (Ο† (head s as)) (tail s as))
\end{code}

For example, descending chains in ordinals can be seen as paths in a
W-type of ordinals. See Iterative.index.