Martin Escardo, Paulo Oliva, 2-27 July 2021

We represent the moves of a history-dependent sequential game by a
dependent-type tree, collected in a type 𝑻.  This is either an empty
tree [] or else has a type X of initial moves at the root, and,
inductively, a family Xf of subtrees indexed by elements of X, which
is written X ∷ Xf. We refer to the family Xf as a forest. We let Xt
range over such trees.

 * Xt ranges over dependent-type trees.
 * Xf ranges over dependent-type forests.

\begin{code}

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

module Games.TypeTrees where

open import Games.Monad
open import MLTT.Spartan
open import UF.FunExt
open import UF.Subsingletons
open import UF.Subsingletons-FunExt

data 𝑻 : Type₁ where
  []  : 𝑻
  _∷_ : (X : Type) (Xf : X β†’ 𝑻) β†’ 𝑻

\end{code}

The type of full paths in a tree Xt, from the root to a leaf, is
inductively defined as follows:

\begin{code}

Path : 𝑻 β†’ Type
Path []       = πŸ™
Path (X ∷ Xf) = Ξ£ x κž‰ X , Path (Xf x)

\end{code}

As discussed above, a play in a game is defined to be such a path.

The idea is that we choose a move x, and then, inductively, a path in
the subtree Xf x.

The variable xs ranges over paths, that is, elements of the type
Path Xt for a dependent-type-tree Xt.

\begin{code}

pattern ⟨⟩        = ⋆
pattern _::_ x xs = (x , xs)

path-head : {X : Type} {Xf : X β†’ 𝑻} β†’ Path (X ∷ Xf) β†’ X
path-head (x :: xs) = x

path-tail : {X : Type} {Xf : X β†’ 𝑻} ((x :: xs) : Path (X ∷ Xf)) β†’ Path (Xf x)
path-tail (x :: xs) = xs

plength : {Xt : 𝑻} β†’ Path Xt β†’ β„•
plength {[]}     ⟨⟩        = 0
plength {X ∷ Xf} (x :: xs) = succ (plength {Xf x} xs)

subpred : {X R : Type} {Xf : X β†’ 𝑻} β†’ ((Ξ£ x κž‰ X , Path (Xf x)) β†’ R) β†’ (x : X) β†’ Path (Xf x) β†’ R
subpred q x xs = q (x :: xs)

\end{code}

NB. An alternative inductive definition of Path is the following,
where, unfortunately, we get a higher type level, and so we won't use
it:

\begin{code}

data Path₁ : 𝑻 β†’ Type₁ where
 []  : Path₁ []
 _∷_ : {X : Type} {Xf : X β†’ 𝑻} (x : X) (xs : Path₁ (Xf x)) β†’ Path₁ (X ∷ Xf)

\end{code}

Equip the internal nodes of a type tree with structure:

\begin{code}

structure : (Type β†’ 𝓀 Μ‡ ) β†’ 𝑻 β†’ 𝓀 Μ‡
structure S []       = πŸ™
structure S (X ∷ Xf) = S X Γ— ((x : X) β†’ structure S (Xf x))

\end{code}

NB. An alternative inductive definition of structure is the following,
where, unfortunately, we get a higher type level, and so we won't use
it:

\begin{code}

data structure₁ (S : Type β†’ 𝓀 Μ‡ ) : 𝑻 β†’ 𝓀 ⁺ Μ‡ where
 []  : structure₁ S []
 _∷_ : {X : Type} {Xf : X β†’ 𝑻} β†’ S X β†’ ((x : X) β†’ structure₁ S (Xf x)) β†’ structure₁ S (X ∷ Xf)

structure-up : (S : Type β†’ 𝓀 Μ‡ ) (Xt : 𝑻) β†’ structure S Xt β†’ structure₁ S Xt
structure-up S []      ⟨⟩         = []
structure-up S (X ∷ Xf) (s :: sf) = s ∷ (Ξ» x β†’ structure-up S (Xf x) (sf x))

structure-down : (S : Type β†’ 𝓀 Μ‡ ) (Xt : 𝑻) β†’ structure₁ S Xt β†’ structure S Xt
structure-down S []      []        = ⟨⟩
structure-down S (X ∷ Xf) (s ∷ sf) = s :: (Ξ» x β†’ structure-down S (Xf x) (sf x))

\end{code}

Xt is hereditarily P if all its internal nodes satisfy P:

\begin{code}

_is-hereditarily_ : 𝑻 β†’ (Type β†’ Type) β†’ Type
[]       is-hereditarily P = πŸ™
(X ∷ Xf) is-hereditarily P = P X Γ— ((x : X) β†’ Xf x is-hereditarily P)

being-hereditary-is-prop : Fun-Ext
                         β†’ (P : Type β†’ Type)
                         β†’ ((X : Type) β†’ is-prop (P X))
                         β†’ (Xt : 𝑻) β†’ is-prop (Xt is-hereditarily P)
being-hereditary-is-prop fe P P-is-prop-valued [] = πŸ™-is-prop
being-hereditary-is-prop fe P P-is-prop-valued (X ∷ Xf) =
 Γ—-is-prop
  (P-is-prop-valued X)
  (Ξ -is-prop fe Ξ» x β†’ being-hereditary-is-prop fe P P-is-prop-valued (Xf x))

\end{code}

The sequence operator for monads is defined on lists, but here we
consider a version on paths of a tree instead:

\begin{code}

path-sequence : (𝓣 : Monad) {Xt : 𝑻} β†’ structure (functor 𝓣) Xt β†’ functor 𝓣 (Path Xt)
path-sequence 𝓣 {[]}     ⟨⟩        = Ξ· 𝓣 ⟨⟩
path-sequence 𝓣 {X ∷ Xf} (t :: tf) = t βŠ—[ 𝓣 ] (Ξ» x β†’ path-sequence 𝓣 {Xf x} (tf x))

\end{code}

The induction principle for 𝑻 is included for the sake of
completeness, but won't be used directly:

\begin{code}

𝑻-induction : (P : 𝑻 β†’ 𝓀 Μ‡ )
            β†’ P []
            β†’ ((X : Type) (Xf : X β†’ 𝑻) β†’ ((x : X) β†’ P (Xf x)) β†’ P (X ∷ Xf))
            β†’ (Xt : 𝑻) β†’ P Xt
𝑻-induction P b f = h
 where
  h : (Xt : 𝑻) β†’ P Xt
  h []       = b
  h (X ∷ Xf) = f X Xf (Ξ» x β†’ h (Xf x))

𝑻-recursion : (A : 𝓀 Μ‡ )
            β†’ A
            β†’ ((X : Type) β†’ (X β†’ 𝑻) β†’ (X β†’ A) β†’ A)
            β†’ 𝑻 β†’ A
𝑻-recursion A = 𝑻-induction (Ξ» _ β†’ A)

𝑻-iteration : (A : 𝓀 Μ‡ )
            β†’ A
            β†’ ((X : Type) β†’ (X β†’ A) β†’ A)
            β†’ 𝑻 β†’ A
𝑻-iteration A a g = 𝑻-induction (Ξ» _ β†’ A) a (Ξ» X Xf β†’ g X)

\end{code}

Here are some examples for the sake of illustration:

\begin{code}

private

 Path' : 𝑻 β†’ Type
 Path' = 𝑻-iteration Type πŸ™ (Ξ» X F β†’ Ξ£ x κž‰ X , F x)

 Path'-[] : Path' [] ＝ πŸ™
 Path'-[] = refl

 Path'-∷ : (X : Type) (Xf : X β†’ 𝑻)
         β†’ Path' (X ∷ Xf) ＝ (Ξ£ x κž‰ X , Path' (Xf x))
 Path'-∷ X Xf = refl

 structure' : (S : Type β†’ 𝓀 Μ‡ ) β†’ 𝑻 β†’ 𝓀 Μ‡
 structure' {𝓀} S = 𝑻-iteration (𝓀 Μ‡ ) πŸ™ (Ξ» X F β†’ S X Γ— ((x : X) β†’ F x))

 structure'-[] : (S : Type β†’ 𝓀 Μ‡ )
               β†’ structure' S [] ＝ πŸ™
 structure'-[] S = refl

 structure'-∷ : (S : Type β†’ 𝓀 Μ‡ ) (X : Type) (Xf : X β†’ 𝑻)
              β†’ structure' S (X ∷ Xf) ＝ S X Γ— ((x : X) β†’ structure' S (Xf x))
 structure'-∷ S X Xf = refl

\end{code}