Martin Escardo, Paulo Oliva, 2022, version of October 2023.

Remark added 11th June 2025. This file is experimental. In particular,
we are not sure our use of the algebra is modelling the intented
notions. It may be that different players need different algebras. For
example, if we are working with the powerset monad, whose algebras are
the sup-lattices, and some players play argmax and some players play
argmin, then it is plausible that the argmax players need an
inf-algebra, whereas the argim players need a sup-algebra. Another
potential issue is the notion of attainability for multi-valued
selection functions and quantifiers.

Warning. This module is a mess. We plan to clean it up soon. At the
moment the proofs are in "blackboard" style (improvised proofs that
work) rather than "article" style (proofs written in a more
presentable way).

This generalizes (but also uses) the file Games.FiniteHistoryDependent
with a monad parameter 𝓣. When 𝓣 is the identity monad 𝕀𝕕, the
original development is obtained. We apply the selection-monad
transformer 𝕁-transf to 𝓣. Notice, however, that the definition of
game is the same. See [1] for background.

The main examples of 𝓣 we have in mind are the powerset monad (for the
Herbrand Functional Interpretation [2]), probability distribution
monads (for mixed strategies) and the reader monad (for alpha-beta
pruning in the file Games.alpha-beta).

[1] M. Escardo and P. Oliva.
    Higher-order Games with Dependent Types (2023)
    https://doi.org/10.1016/j.tcs.2023.114111
    Available in TypeTopology at Games.FiniteHistoryDependent.

[2] M. Escardo and P. Oliva.
    The Herbrand functional interpretation of the double negation shift (2017)
    https://doi.org/10.1017/jsl.2017.8
    (Not available in TypeTopology at the time of writing (October 2023).)

\begin{code}

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

open import Games.TypeTrees
open import MonadOnTypes.Monad
open import MonadOnTypes.J-transf
open import MonadOnTypes.K
open import MLTT.Spartan hiding (J)
open import UF.FunExt

module Games.FiniteHistoryDependentMonadic
        (fe : Fun-Ext)
        (𝕋  : Monad)
        (R  : Type)
        (𝓐  : Algebra 𝕋 R)
 where

open import Games.FiniteHistoryDependent R
     using (𝓚 ; Game ; game ; sequenceᴷ ; optimal-outcome)

open Game

fext : DN-funext 𝓤₀ 𝓤₀
fext = dfunext fe

open K-definitions R
open T-definitions 𝕋
open α-definitions 𝕋 R 𝓐
open JT-definitions 𝕋 R fe
open JT-algebra-definitions 𝕋 R 𝓐 fe

JT-remark : JT ＝ λ X → (X → T R) → T X
JT-remark = by-definition

\end{code}

The types of trees with JT and KT structure.

\begin{code}

𝓙𝓣 : 𝑻 → Type
𝓙𝓣 = structure JT

𝓚𝓣 : 𝑻 → Type
𝓚𝓣 = structure KT

sequenceᴶᵀ : {Xt : 𝑻} → 𝓙𝓣 Xt → JT (Path Xt)
sequenceᴶᵀ = path-sequence 𝕁𝕋

T-Strategy : 𝑻 → Type
T-Strategy = structure T

T-strategic-path : {Xt : 𝑻} → T-Strategy Xt → T (Path Xt)
T-strategic-path = path-sequence 𝕋

is-in-T-equilibrium : {X : Type} {Xf : X → 𝑻}
                      (q : (Σ x ꞉ X , Path (Xf x)) → R)
                      (ϕ : K X)
                    → T-Strategy (X ∷ Xf)
                    → Type
is-in-T-equilibrium {X} {Xf} q ϕ σt@(σ :: σf)  =
 α-extᵀ q (T-strategic-path σt) ＝ ϕ (λ x → α-curryᵀ q x (T-strategic-path (σf x)))

\end{code}

Subgame perfect equilibrium with respect to the monad T.

\begin{code}

is-in-T-sgpe' : {Xt : 𝑻} → 𝓚 Xt → (Path Xt → R) → T-Strategy Xt → Type
is-in-T-sgpe' {[]}     ⟨⟩        q ⟨⟩           = 𝟙
is-in-T-sgpe' {X ∷ Xf} (ϕ :: ϕf) q σt@(σ :: σf) =
    is-in-T-equilibrium q ϕ σt
  × ((x : X) → is-in-T-sgpe' {Xf x} (ϕf x) (subpred q x) (σf x))

is-in-T-sgpe : (G : Game) → T-Strategy (Xt G) → Type
is-in-T-sgpe (game Xt q ϕt) = is-in-T-sgpe' {Xt} ϕt q

\end{code}

The main lemma is that the optimal outcome is the same thing as the
application of the outcome function to the path induced by a strategy
in perfect subgame equilibrium.

\begin{code}

T-sgpe-lemma : (Xt : 𝑻) (ϕt : 𝓚 Xt) (q : Path Xt → R) (σt : T-Strategy Xt)
             → is-in-T-sgpe' ϕt q σt
             → α-extᵀ q (T-strategic-path σt) ＝ sequenceᴷ ϕt q
T-sgpe-lemma [] ⟨⟩ q ⟨⟩ ⟨⟩ =
  α-extᵀ q (T-strategic-path ⟨⟩) ＝⟨ refl ⟩
  α (extᵀ (ηᵀ ∘ q) (ηᵀ ⟨⟩))      ＝⟨ ap α (unitᵀ (ηᵀ ∘ q) ⟨⟩) ⟩
  α (ηᵀ (q ⟨⟩))                  ＝⟨ α-unitᵀ (q ⟨⟩) ⟩
  q ⟨⟩                           ＝⟨ refl ⟩
  sequenceᴷ ⟨⟩ q                 ∎
T-sgpe-lemma (X ∷ Xf) (ϕ :: ϕt) q (σ :: σf) (h :: t) =
 α-extᵀ q (T-strategic-path (σ :: σf))            ＝⟨ h ⟩
 ϕ (λ x → α-curryᵀ q x (T-strategic-path (σf x))) ＝⟨ ap ϕ (fext IH) ⟩
 ϕ (λ x → sequenceᴷ (ϕt x) (subpred q x))         ＝⟨ refl ⟩
 sequenceᴷ (ϕ :: ϕt) q                            ∎
  where
   IH : (x : X) → α-curryᵀ q x (T-strategic-path (σf x))
                ＝ sequenceᴷ (ϕt x) (subpred q x)
   IH x = T-sgpe-lemma (Xf x) (ϕt x) (subpred q x) (σf x) (t x)

\end{code}

This can be reformulated as follows in terms of the type of games:

\begin{code}

T-optimality-theorem : (G : Game) (σt : T-Strategy (Xt G))
                     → is-in-T-sgpe G σt
                     → α-extᵀ (q G) (T-strategic-path σt)
                     ＝ optimal-outcome G
T-optimality-theorem (game Xt q ϕt) = T-sgpe-lemma Xt ϕt q

\end{code}

We now show how to use selection functions to compute a sgpe strategy.

\begin{code}

T-selection-strategy : {Xt : 𝑻} → 𝓙𝓣 Xt → (Path Xt → R) → T-Strategy Xt
T-selection-strategy {[]}     ⟨⟩           q = ⟨⟩
T-selection-strategy {X ∷ Xf} εt@(ε :: εf) q = σ :: σf
 where
  t : T (Path (X ∷ Xf))
  t = sequenceᴶᵀ εt (ηᵀ ∘ q)

  σ : T X
  σ = mapᵀ path-head t

  σf : (x : X) → T-Strategy (Xf x)
  σf x = T-selection-strategy {Xf x} (εf x) (subpred q x)

\end{code}

For the next technical lemma, we need the monad T to satisfy the
condition extᵀ-const defined in MonadOnTypes.Monads, which says that the
Kleisli extension of a constant function is itself constant. Ohad
Kammar pointed out to us that this condition is equivalent to the
monad being affine. A proof is included in the module MonadOnTypes.Monad.

TODO. Explain the intuition of the condition extᵀ-const and
equivalents.

\begin{code}

mapᵀ-path-head-lemma' : {X : Type}
                        {Xf : X → 𝑻}
                        (a : T X)
                        (b : (x : X) → T (Path (Xf x)))
                      → mapᵀ path-head (a ⊗ᵀ b)
                      ＝ extᵀ (λ x → extᵀ (λ _ → ηᵀ x) (b x)) a
mapᵀ-path-head-lemma' {X} {Xf} a b =
  mapᵀ path-head (a ⊗ᵀ b)                                  ＝⟨ refl ⟩
  extᵀ (ηᵀ ∘ path-head) (a ⊗ᵀ b)                           ＝⟨ refl ⟩
  extᵀ g (a ⊗ᵀ b)                                          ＝⟨ refl ⟩
  extᵀ g (extᵀ (λ x → mapᵀ (x ::_) (b x)) a)               ＝⟨ refl ⟩
  extᵀ g (extᵀ (λ x → extᵀ (ηᵀ ∘ (x ::_)) (b x)) a)        ＝⟨ ⦅1⦆ ⟩
  extᵀ (extᵀ g ∘ (λ x → extᵀ (ηᵀ ∘ (x ::_)) (b x))) a      ＝⟨ refl ⟩
  extᵀ (extᵀ g ∘ (λ x → extᵀ (f x) (b x))) a               ＝⟨ refl ⟩
  extᵀ (λ x → extᵀ g (extᵀ (f x) (b x))) a                 ＝⟨ refl ⟩
  extᵀ (λ x → (extᵀ g ∘ extᵀ (f x)) (b x)) a               ＝⟨ ⦅2⦆ ⟩
  extᵀ (λ x → extᵀ (extᵀ g ∘ (f x)) (b x)) a               ＝⟨ refl ⟩
  extᵀ (λ x → extᵀ (λ xs → extᵀ g (ηᵀ (x :: xs))) (b x)) a ＝⟨ ⦅3⦆ ⟩
  extᵀ (λ x → extᵀ (λ xs → g (x :: xs)) (b x)) a           ＝⟨ refl ⟩
  extᵀ (λ x → extᵀ (λ _ → ηᵀ x) (b x)) a                   ∎
 where
  g : Path (X ∷ Xf) → T X
  g = ηᵀ ∘ path-head

  f : (x : X) → Path (Xf x) → T (Path (X ∷ Xf))
  f x = ηᵀ ∘ (x ::_)

  I : ∀ x → (extᵀ g ∘ extᵀ (f x)) (b x) ＝ extᵀ (extᵀ g ∘ (f x)) (b x)
  I x = (assocᵀ g (f x) (b x))⁻¹

  II : (x : X) (xs : Path (Xf x)) → extᵀ g (ηᵀ (x :: xs)) ＝ g (x :: xs)
  II x xs = unitᵀ g (x :: xs)

  ⦅1⦆ = (assocᵀ g (λ x → extᵀ (f x) (b x)) a)⁻¹
  ⦅2⦆ = ap (λ - → extᵀ - a) (fext I)
  ⦅3⦆ = ap (λ - →  extᵀ (λ x → extᵀ (- x) (b x)) a) (fext (λ x → fext (II x)))


mapᵀ-path-head-lemma : {X : Type} {Xf : X → 𝑻}
                       (a : T X) (b : (x : X) → T (Path (Xf x)))
                     → ext-const 𝕋
                     → mapᵀ path-head (a ⊗ᵀ b) ＝ a
mapᵀ-path-head-lemma {X} {Xf} a b ext-const =
  mapᵀ path-head (a ⊗ᵀ b)                                  ＝⟨ ⦅1⦆ ⟩
  extᵀ (λ x → extᵀ (λ _ → ηᵀ x) (b x)) a                   ＝⟨ ⦅2⦆ ⟩
  extᵀ ηᵀ a                                                ＝⟨ extᵀ-η a ⟩
  a                                                        ∎
 where
  ⦅1⦆ = mapᵀ-path-head-lemma' a b
  ⦅2⦆ = ap (λ - → extᵀ - a) (fext (λ x → ext-const (ηᵀ x) (b x)))

\end{code}

We also need the following technical lemma, which expresses the tensor
_⊗ᴶᵀ_ in terms of the tensor _⊗ᵀ_ as in Lemma 2.3 of reference [2]
above.

\begin{code}

module _ {X  : Type}
         {Y  : X → Type}
         (ε  : JT X)
         (δ  : (x : X) → JT (Y x))
 where

 private
  ν : ((Σ x ꞉ X , Y x) → T R) → (x : X) → T (Y x)
  ν q x = δ x (λ y → q (x , y))

  τ : ((Σ x ꞉ X , Y x) → T R) → T X
  τ q = ε (λ x → extᵀ (λ y → q (x , y)) (ν q x))

 ⊗ᴶᵀ-in-terms-of-⊗ᵀ : (q : (Σ x ꞉ X , Y x) → T R)
                    → (ε ⊗ᴶᵀ δ) q ＝ τ q ⊗ᵀ ν q
 ⊗ᴶᵀ-in-terms-of-⊗ᵀ q =
    (ε ⊗ᴶᵀ δ) q                                          ＝⟨ refl ⟩
    extᴶᵀ (λ x → extᴶᵀ (λ y _ → ηᵀ (x , y)) (δ x)) ε q   ＝⟨ ⦅1⦆ ⟩
    extᴶᵀ Θ ε q                                          ＝⟨ refl ⟩
    extᵀ (λ x → Θ x q) (ε (λ x → extᵀ q (Θ x q)))        ＝⟨ ⦅2⦆ ⟩
    extᵀ (λ x → Θ x q) (τ q)                             ＝⟨ refl ⟩
    τ q ⊗ᵀ ν q                                           ∎
     where
      Θ : X → JT (Σ x ꞉ X , Y x)
      Θ x r = extᵀ (λ y → ηᵀ (x , y)) (ν r x)

      I : (λ x → extᴶᵀ (λ y _ → ηᵀ (x , y)) (δ x)) ＝ Θ
      I = fext (λ x →
          fext (λ r → ap (λ - → extᵀ (λ y → ηᵀ (x , y)) (δ x (λ y → - (x , y))))
                         (fext (unitᵀ r))))

      ⦅1⦆ = ap (λ - → extᴶᵀ - ε q) I

      II : ∀ x → extᵀ q ∘ extᵀ (λ y → ηᵀ (x , y)) ＝ extᵀ (λ y → q (x , y))
      II x = extᵀ q ∘ extᵀ (λ y → ηᵀ (x , y))               ＝⟨ ⦅i⦆ ⟩
             (λ x' → extᵀ (extᵀ q ∘ (λ y → ηᵀ (x , y))) x') ＝⟨ refl ⟩
             extᵀ (λ y → ((extᵀ q) ∘ ηᵀ) (x , y))           ＝⟨ ⦅ii⦆ ⟩
             extᵀ (λ y → q (x , y))                         ∎
       where
        ⦅i⦆  = fext (λ x' → (assocᵀ q (λ y → ηᵀ (x , y)) x')⁻¹)
        ⦅ii⦆ = ap extᵀ (fext (λ y → unitᵀ q (x , y)))

      III : ε (λ x → extᵀ q (extᵀ (λ y → ηᵀ (x , y)) (ν q x))) ＝ τ q
      III = ap ε (fext (λ x → ap (λ - → - (ν q x)) (II x)))

      ⦅2⦆ = ap (extᵀ (λ x → Θ x q)) III

\end{code}

The following is the main lemma of this file.

Given a selection tree εt over Xt and an outcome function q, we can
either sequence εt and apply it to q to obtain a monadic path on Xt,
or we can first use εt to calculate a strategy on Xt and derive its
monadic strategic path. The lemma says that these are the same path.

\begin{code}

T-main-lemma : ext-const 𝕋
             → {Xt : 𝑻} (εt : 𝓙𝓣 Xt) (q : Path Xt → R)
             → sequenceᴶᵀ εt (ηᵀ ∘ q)
             ＝ T-strategic-path (T-selection-strategy εt q)
T-main-lemma ext-const {[]}     ⟨⟩           q = refl
T-main-lemma ext-const {X ∷ Xf} εt@(ε :: εf) q = γ
 where
  δ : (x : X) → JT (Path (Xf x))
  δ x = sequenceᴶᵀ {Xf x} (εf x)

  q' : (x : X) → Path (Xf x) → T R
  q' x = ηᵀ ∘ subpred q x

  σf : (x : X) → T-Strategy (Xf x)
  σf x = T-selection-strategy {Xf x} (εf x) (subpred q x)

  b c : (x : X) → T (Path (Xf x))
  b x = δ x (q' x)
  c x = T-strategic-path (σf x)

  IH : b ∼ c
  IH x = T-main-lemma ext-const (εf x) (subpred q x)

  σ : T X
  σ = mapᵀ path-head (sequenceᴶᵀ εt (ηᵀ ∘ q))

  I = ε (λ x → extᵀ (q' x) (c x))                       ＝⟨ ⦅1⦆ ⟩
      mapᵀ path-head (ε (λ x → extᵀ (q' x) (c x)) ⊗ᵀ c) ＝⟨ ⦅2⦆ ⟩
      mapᵀ path-head (ε (λ x → extᵀ (q' x) (b x)) ⊗ᵀ b) ＝⟨ ⦅3⦆ ⟩
      mapᵀ path-head ((ε ⊗ᴶᵀ δ) (ηᵀ ∘ q))               ＝⟨ refl ⟩
      mapᵀ path-head (sequenceᴶᵀ εt (ηᵀ ∘ q))           ＝⟨ refl ⟩
      σ                                                 ∎
   where
    ⦅1⦆ = (mapᵀ-path-head-lemma (ε (λ x → extᵀ (q' x) (c x))) c ext-const)⁻¹
    ⦅2⦆ = ap (λ - → mapᵀ path-head (ε (λ x → extᵀ (q' x) (- x)) ⊗ᵀ -))
            (fext (λ x → (IH x)⁻¹))
    ⦅3⦆ = (ap (mapᵀ path-head) (⊗ᴶᵀ-in-terms-of-⊗ᵀ ε δ (ηᵀ ∘ q)))⁻¹

  γ : sequenceᴶᵀ (ε :: εf) (ηᵀ ∘ q)
    ＝ T-strategic-path (T-selection-strategy (ε :: εf) q)
  γ = sequenceᴶᵀ (ε :: εf) (ηᵀ ∘ q)                    ＝⟨ refl ⟩
      (ε ⊗ᴶᵀ δ) (ηᵀ ∘ q)                                ＝⟨ ⦅1⦆ ⟩
      ε (λ x → extᵀ (q' x) (b x)) ⊗ᵀ b                  ＝⟨ ⦅2⦆ ⟩
      (ε (λ x → extᵀ (q' x) (c x)) ⊗ᵀ c)                ＝⟨ ⦅3⦆ ⟩
      σ ⊗ᵀ c                                            ＝⟨ refl ⟩
      σ ⊗ᵀ (λ x → T-strategic-path {Xf x} (σf x))       ＝⟨ refl ⟩
      T-strategic-path (σ :: σf)                        ＝⟨ refl ⟩
      T-strategic-path (T-selection-strategy (ε :: εf) q) ∎
   where
    ⦅1⦆ = ⊗ᴶᵀ-in-terms-of-⊗ᵀ ε δ (ηᵀ ∘ q)
    ⦅2⦆ = ap (λ - → ε (λ x → extᵀ (q' x) (- x)) ⊗ᵀ -) (fext IH)
    ⦅3⦆ = ap (_⊗ᵀ c) I

\end{code}

Is α-Overlineᵀ useful?

\begin{code}

{-
α-Overlineᵀ : {Xt : 𝑻} → 𝓙𝓣 Xt → 𝓚𝓣 Xt
α-Overlineᵀ {[]}     ⟨⟩        = ⟨⟩
α-Overlineᵀ {X ∷ Xf} (ε :: εf) = α-overlineᵀ ε :: λ x → α-Overlineᵀ {Xf x} (εf x)
-}

_Attainsᵀ_ : {Xt : 𝑻} → 𝓙𝓣 Xt → 𝓚 Xt → Type
_Attainsᵀ_ {[]}     ⟨⟩        ⟨⟩        = 𝟙
_Attainsᵀ_ {X ∷ Xf} (ε :: εf) (ϕ :: ϕf) = (ε α-attainsᵀ ϕ)
                                        × ((x : X) → (εf x) Attainsᵀ (ϕf x))

T-selection-strategy-lemma : ext-const 𝕋
                           → {Xt : 𝑻} (εt : 𝓙𝓣 Xt) (ϕt : 𝓚 Xt) (q : Path Xt → R)
                           → εt Attainsᵀ ϕt
                           → is-in-T-sgpe' ϕt q (T-selection-strategy εt q)
T-selection-strategy-lemma ext-const {[]}     ⟨⟩           ⟨⟩           q ⟨⟩           = ⟨⟩
T-selection-strategy-lemma ext-const {X ∷ Xf} εt@(ε :: εf) ϕt@(ϕ :: ϕf) q at@(a :: af) = γ
 where
  have-a : (p : X → T R) → α (extᵀ p (ε p)) ＝ ϕ (α ∘ p)
  have-a = a

  σf : (x : X) → structure T (Xf x)
  σf x = T-selection-strategy {Xf x} (εf x) (subpred q x)

  σ : T X
  σ = mapᵀ path-head (sequenceᴶᵀ εt (ηᵀ ∘ q))

  p : X → T R
  p x = mapᵀ (subpred q x) (T-strategic-path (σf x))

  I = λ x → α-curryᵀ q x (T-strategic-path (σf x)) ＝⟨ refl ⟩
            α-extᵀ (subpred q x) (T-strategic-path (σf x)) ＝⟨ refl ⟩
            α (mapᵀ (subpred q x) (T-strategic-path (σf x))) ∎

  have-a' : α (extᵀ p (ε p)) ＝ ϕ (α ∘ p)
  have-a' = a p

  t : T (Path (X ∷ Xf))
  t = T-strategic-path (σ :: σf)

  III : ε p ＝ σ
  III = ε p ＝⟨ refl ⟩
        ε (λ x → mapᵀ (subpred q x) (T-strategic-path (σf x))) ＝⟨ refl ⟩
        ε (λ x → mapᵀ (subpred q x) (T-strategic-path (T-selection-strategy {Xf x} (εf x) (subpred q x)))) ＝⟨ III₀ ⟩
        ε (λ x → mapᵀ (subpred q x) (sequenceᴶᵀ (εf x) (subpred (ηᵀ ∘ q) x))) ＝⟨ refl ⟩
        ε (λ x → mapᵀ (subpred q x) (ν x)) ＝⟨ refl ⟩
        ε (λ x → extᵀ (subpred (ηᵀ ∘ q) x) (ν x)) ＝⟨ refl ⟩
        τ ＝⟨ III₁ ⟩
        mapᵀ path-head (τ ⊗ᵀ ν) ＝⟨ III₂ ⟩
        mapᵀ path-head ((ε ⊗ᴶᵀ (λ x → sequenceᴶᵀ (εf x))) (ηᵀ ∘ q)) ＝⟨ refl ⟩
        mapᵀ path-head (sequenceᴶᵀ εt (ηᵀ ∘ q)) ＝⟨ refl ⟩
        σ ∎
        where
         ν : (x : X) → T (Path (Xf x))
         ν x = sequenceᴶᵀ (εf x) (subpred (ηᵀ ∘ q) x)

         τ : T X
         τ = ε (λ x → extᵀ (subpred (ηᵀ ∘ q) x) (ν x))

         III₀ = ap (λ - → ε (λ x → mapᵀ (subpred q x) (- x))) (dfunext fe (λ x → (T-main-lemma ext-const (εf x) (subpred q x))⁻¹))
         III₁ = (mapᵀ-path-head-lemma τ ν ext-const)⁻¹
         III₂ = ap (mapᵀ path-head) ((⊗ᴶᵀ-in-terms-of-⊗ᵀ {X} {λ x → Path (Xf x)} ε (λ x → sequenceᴶᵀ (εf x)) (ηᵀ ∘ q)) ⁻¹)

  II : α (extᵀ p (ε p)) ＝ α-extᵀ q t
  II = α (extᵀ p (ε p)) ＝⟨ II₀ ⟩
       α (extᵀ p σ) ＝⟨ refl ⟩
       α (extᵀ (λ x → mapᵀ (subpred q x) (T-strategic-path (σf x))) σ) ＝⟨ refl ⟩
       α (extᵀ (λ x → extᵀ (ηᵀ ∘ subpred q x) (T-strategic-path (σf x))) σ) ＝⟨ II₁ ⟩
       α (extᵀ (λ x →  extᵀ (λ xs → extᵀ (ηᵀ ∘ q) (ηᵀ (x :: xs))) (T-strategic-path (σf x))) σ) ＝⟨ refl ⟩
       α (extᵀ (λ x →  extᵀ (extᵀ (ηᵀ ∘ q) ∘ (λ xs → ηᵀ (x :: xs))) (T-strategic-path (σf x))) σ) ＝⟨ II₂ ⟩
       α (extᵀ (λ x → extᵀ (ηᵀ ∘ q) (extᵀ (λ xs → ηᵀ (x :: xs)) (T-strategic-path (σf x)))) σ) ＝⟨ refl ⟩
       α (extᵀ (extᵀ (λ x → ηᵀ (q x)) ∘ (λ x → mapᵀ (λ y → x , y) (T-strategic-path (σf x)))) σ) ＝⟨ II₃ ⟩
       α (extᵀ (ηᵀ ∘ q) (extᵀ (λ x → mapᵀ (λ y → x , y) (T-strategic-path (σf x))) σ)) ＝⟨ refl ⟩
       α (extᵀ (ηᵀ ∘ q) (σ ⊗ᵀ λ x → T-strategic-path (σf x))) ＝⟨ refl ⟩
       α (extᵀ (ηᵀ ∘ q) (T-strategic-path (σ :: σf))) ＝⟨ refl ⟩
       α (mapᵀ q (T-strategic-path (σ :: σf))) ＝⟨ refl ⟩
       α (mapᵀ q (T-strategic-path (σ :: σf))) ＝⟨ refl ⟩
       α (mapᵀ q t) ＝⟨ refl ⟩
       α-extᵀ q t ∎
        where
         II₀ = ap (λ - → α (extᵀ p -)) III
         II₁ = ap (λ - → α (extᵀ (λ x →  extᵀ (λ xs → - x xs) (T-strategic-path (σf x))) σ)) (dfunext fe (λ x → dfunext fe (λ xs → (unitᵀ (ηᵀ ∘ q) (x :: xs))⁻¹)))
         II₂ = ap (λ - → α (extᵀ (λ x → - x) σ)) (dfunext fe (λ x → assocᵀ (ηᵀ ∘ q) (λ xs → ηᵀ (x :: xs)) (T-strategic-path (σf x))))
         II₃ = ap α (assocᵀ (ηᵀ ∘ q) (λ x → mapᵀ (λ y → x , y) (T-strategic-path (σf x))) σ)

  γ' : (α-extᵀ q t ＝ ϕ (α ∘ p))
     × (((x : X) → is-in-T-sgpe' {Xf x} (ϕf x) (subpred q x) (σf x)))
  γ' = (α-extᵀ q t ＝⟨ II ⁻¹ ⟩
       α (extᵀ p (ε p)) ＝⟨ a p ⟩
       ϕ (α ∘ p) ∎) ,
       (λ x → T-selection-strategy-lemma ext-const (εf x) (ϕf x) (subpred q x) (af x))

  γ : is-in-T-sgpe' (ϕ :: ϕf) q (T-selection-strategy (ε :: εf) q)
  γ = γ'

main-theorem : ext-const 𝕋
             → (G : Game)
               (εt : 𝓙𝓣 (Xt G))
             → εt Attainsᵀ (ϕt G)
             → is-in-T-sgpe G (T-selection-strategy εt (q G))
main-theorem ext-const G εt = T-selection-strategy-lemma ext-const εt (ϕt G) (q G)

\end{code}

Alternative, non-inductive definition of T-optimality. We don't have
any use for it, but it is useful for comparison with the classical
notion. Partial, possibly empty, paths in 𝑻's, and related notions.

\begin{code}

pPath : 𝑻 → Type
pPath []       = 𝟙
pPath (X ∷ Xf) = 𝟙 + (Σ x ꞉ X , pPath (Xf x))

sub𝑻 : (Xt : 𝑻) → pPath Xt → 𝑻
sub𝑻 []       ⟨⟩              = []
sub𝑻 (X ∷ Xf) (inl ⟨⟩)        = X ∷ Xf
sub𝑻 (X ∷ Xf) (inr (x :: xs)) = sub𝑻 (Xf x) xs

Subpred : {Xt : 𝑻} → (Path Xt → R) → (xs : pPath Xt) → Path (sub𝑻 Xt xs) → R
Subpred {[]} q ⟨⟩ ⟨⟩ = q ⟨⟩
Subpred {X ∷ Xf} q (inl ⟨⟩) (y :: ys) = q (y :: ys)
Subpred {X ∷ Xf} q (inr (x :: xs)) ys = Subpred {Xf x} (subpred q x) xs ys

sub𝓚 : {Xt : 𝑻} → 𝓚 Xt → (xs : pPath Xt) → 𝓚 (sub𝑻 Xt xs)
sub𝓚 {[]} ϕt ⟨⟩ = ⟨⟩
sub𝓚 {X ∷ Xf} ϕt (inl ⟨⟩) = ϕt
sub𝓚 {X ∷ Xf} (ϕ :: ϕf) (inr (x :: xs)) = sub𝓚 {Xf x} (ϕf x) xs

sub𝓙𝓣 : {Xt : 𝑻} → 𝓙𝓣 Xt → (xs : pPath Xt) → 𝓙𝓣 (sub𝑻 Xt xs)
sub𝓙𝓣 {[]} εt ⟨⟩ = ⟨⟩
sub𝓙𝓣 {X ∷ Xf} εt (inl ⟨⟩) = εt
sub𝓙𝓣 {X ∷ Xf} (ε :: εf) (inr (x :: xs)) = sub𝓙𝓣 {Xf x} (εf x) xs

subgame : (G : Game) → pPath (Xt G) → Game
subgame (game Xt q ϕt) xs = game (sub𝑻 Xt xs) (Subpred q xs) (sub𝓚 ϕt xs)

sub-T-Strategy : {Xt : 𝑻} → T-Strategy Xt → (xs : pPath Xt) → T-Strategy (sub𝑻 Xt xs)
sub-T-Strategy {[]}     ⟨⟩        ⟨⟩              = ⟨⟩
sub-T-Strategy {X ∷ Xf} (σ :: σf) (inl ⟨⟩)        = σ :: σf
sub-T-Strategy {X ∷ Xf} (σ :: σf) (inr (x :: xs)) = sub-T-Strategy {Xf x} (σf x) xs

is-in-T-equilibrium' : (G : Game) → T-Strategy (Xt G) → Type
is-in-T-equilibrium' (game []       q ⟨⟩)       ⟨⟩ = 𝟙
is-in-T-equilibrium' (game (X ∷ Xf) q (ϕ :: _)) σt = is-in-T-equilibrium q ϕ σt

is-in-T-sgpe₂ : (G : Game) (σ : T-Strategy (Xt G)) → Type
is-in-T-sgpe₂ G σ =
 (xs : pPath (Xt G)) → is-in-T-equilibrium' (subgame G xs) (sub-T-Strategy σ xs)

T-sgpe-equiv : (G : Game) (σ : T-Strategy (Xt G))
             → is-in-T-sgpe  G σ
             ↔ is-in-T-sgpe₂ G σ
T-sgpe-equiv (game Xt q ϕt) σ = I ϕt q σ , II ϕt q σ
 where
  I : {Xt : 𝑻} (ϕt : 𝓚 Xt) (q : Path Xt → R) (σ : T-Strategy Xt)
    → is-in-T-sgpe (game Xt q ϕt) σ → is-in-T-sgpe₂ (game Xt q ϕt) σ
  I {[]}     ⟨⟩        q ⟨⟩        ⟨⟩        ⟨⟩              = ⟨⟩
  I {X ∷ Xf} (ϕ :: ϕf) q (σ :: σf) (i :: _)  (inl ⟨⟩)        = i
  I {X ∷ Xf} (ϕ :: ϕf) q (σ :: σf) (_ :: is) (inr (x :: xs)) =
    I {Xf x} (ϕf x) (subpred q x) (σf x) (is x) xs

  II : {Xt : 𝑻} (ϕt : 𝓚 Xt) (q : Path Xt → R) (σ : T-Strategy Xt)
    → is-in-T-sgpe₂ (game Xt q ϕt) σ → is-in-T-sgpe (game Xt q ϕt) σ
  II {[]}     ⟨⟩        q ⟨⟩        j = ⟨⟩
  II {X ∷ Xf} (ϕ :: ϕf) q (σ :: σf) j =
     j (inl ⟨⟩) ,
     (λ x → II {Xf x} (ϕf x) (subpred q x) (σf x) (λ xs → j (inr (x :: xs))))


{-
T-sgpe-equiv : (G : Game) (σ : T-Strategy (Xt G))
             → is-in-T-sgpe G σ ↔ is-in-T-sgpe₂ G σ
T-sgpe-equiv (game Xt q ϕt) σ = I ϕt q σ , II ϕt q σ

is-in-subgame-perfect-equilibrium : (G : Game) → 𝓙𝓣 (Xt G) → Type
is-in-subgame-perfect-equilibrium G εt =

 (xs : pPath (Xt G)) → is-in-head-equilibrium (subgame G xs) (sub𝓙𝓣 εt xs)

-}
\end{code}