Game functor

The type of games IGame is an inductive type, with a single constructor ofSets taking in two small sets of games and outputting a new game. This suggests the definition:

inductive IGame : Type (u + 1)
  | ofSets (s t : Set IGame) [Small.{u} s] [Small.{u} t] : IGame

However, the kernel does not accept this, as Set IGame = IGame → Prop contains a non-positive occurence of IGame (see counterexamples.org for an explanation of what this is and why it's disallowed). We can get around this technical limitation using the machinery of QPFs (quotients of polynomial functors). We define a functor GameFunctor by

def GameFunctor (α : Type (u + 1)) : Type (u + 1) :=
  {s : Set α × Set α // Small.{u} s.1 ∧ Small.{u} s.2}

We can prove that this is a QPF, which then allows us to build its initial algebra through QPF.Fix, which is exactly the inductive type IGame. As a bonus, we're able to describe the coinductive type of loopy games LGame as the final coalgebra QPF.Cofix of the exact same functor.

def GameFunctor (α : Type (u + 1)) : Type (u + 1)

The functor from a type into the subtype of small pairs of sets in that type.

This is the quotient of a polynomial functor. The type IGame of well-founded games is defined as the initial algebra of that QPF, while the type LGame of loopy games is defined as its final coalgebra.

In other words, IGame and LGame have the following descriptions (which don't work verbatim due to various Lean limitations):

inductive IGame : Type (u + 1)
  | ofSets (s t : Set IGame) [Small.{u} s] [Small.{u} t] : IGame

coinductive LGame : Type (u + 1)
  | ofSets (s t : Set LGame) [Small.{u} s] [Small.{u} t] : LGame

Equations

• GameFunctor α = { s : Set α × Set α // Small.{?u.7, ?u.7 + 1} ↑s.1 ∧ Small.{?u.7, ?u.7 + 1} ↑s.2 }

theorem GameFunctor.ext {α : Type (u + 1)} {x y : GameFunctor α} : ↑x = ↑y → x = y

theorem GameFunctor.ext_iff {α : Type (u + 1)} {x y : GameFunctor α} : x = y ↔ ↑x = ↑y

instance GameFunctor.instSmallElemFstSetValProdAndSnd {α : Type (u + 1)} (x : GameFunctor α) : Small.{u, u + 1} ↑(↑x).1

instance GameFunctor.instSmallElemSndSetValProdAndFst {α : Type (u + 1)} (x : GameFunctor α) : Small.{u, u + 1} ↑(↑x).2

instance GameFunctor.instFunctor : Functor GameFunctor

Equations

• GameFunctor.instFunctor = { map := fun {α β : Type (?u.14 + 1)} (f : α → β) (s : GameFunctor α) => ⟨(f '' (↑s).1, f '' (↑s).2), ⋯⟩ }

theorem GameFunctor.map_def {α β : Type (u_1 + 1)} (f : α → β) (s : GameFunctor α) : f <$> s = ⟨(f '' (↑s).1, f '' (↑s).2), ⋯⟩

noncomputable instance GameFunctor.instQPF : QPF GameFunctor

Equations

• One or more equations did not get rendered due to their size.