Universe polymorphism in `QPF`

Stream: mathlib4

[Aaron Liu]

We are using docs#QPF.Fix and docs#QPF.Cofix in combinatorial games to construct the type of games and the type of loopy games (see #combinatorial-games > Loopy games @ 💬 and subsequent discussion for details). Unfortunately, docs#QPF.Fix.rec is not sufficiently universe polymorphic to be useful. This doesn't happen with docs#PFunctor.W because they don't provide a recursor PFunctor is bundled and QPF is a mixin. This means if you have a functor F : Type u → Type v which is QPF.{u, u', v} F then when writing F α you have to have α : Type u, but if you have a P : PFunctor.{u, v} then P α works for any α : Type w.

The same problem happens with docs#QPF.Cofix.corec, and docs#PFunctor.M.corec does not have this problem.

[Aaron Liu]

Looking through the loogle results, it looks like there are no instances for docs#QPF or docs#MvQPF except for docs#MvQPF.Prj.mvqpf

[Aaron Liu]

I tried bundling QPF. Here's what I've done so far:

So QPF in mathlib right now is implemented is a thing you put on a functor

class QPF (F : Type u → Type v) extends Functor F where
  P : PFunctor.{u, u'}
  abs : ∀ {α}, P α → F α
  repr : ∀ {α}, F α → P α
  abs_repr : ∀ {α} (x : F α), abs (repr x) = x
  abs_map : ∀ {α β} (f : α → β) (p : P α), abs (P.map f p) = f <$> abs p

which is a problem because F only takes Type u so you can't use it with a Type v. So we want some other formulation that F becomes a definition which is universe-polymorphic, like how docs#PFunctor.Obj works with types of any universe. Since it's a QPF is Quotient of a Polynomial Functor, I decided to implement it as a Quotient of the action of a polynomial functor P by a given setoid setoid.

structure QPF.{u, uA, uB} : Type (max u uA uB + 1) where
  P : PFunctor.{uA, uB}
  setoid (α : Type u) : Setoid (P α)
  mapsto (α β : Type u) (f : α → β) : setoid α ≤ (setoid β).comap (P.map f)

To be able to map by a function f, setoid has to satisfy mapsto, otherwise two elements related in setoid α could be mapped to different elements not related by setoid β.

But this doesn't work, we still have the universe u in the type of QPF, so a QPF.{u, uA, uB} can't be used with a Type v. So what I found out is that for setoid we actually don't need to specify it for all of α : Type u, it suffices to say what happens when α is below a certain cardinality and then everything else is determined uniquely. So this is what I have right now:

@[pp_with_univ, nolint checkUnivs]
public structure QPF.{uA, uB} : Type (max uA uB + 1) where
  P : PFunctor.{uA, uB}
  setoid (s : Set (ℕ ⊕ Sigma P.B)) : Setoid (P s)
  mapsto (s t : Set (ℕ ⊕ Sigma P.B)) (f : s → t) : setoid s ≤ (setoid t).comap (P.map f)

and then I define

variable (α) in
public noncomputable def inducedSetoid : Setoid (F.P α) := ...

public theorem inducedSetoid_coherent (f : α → β) :
    F.inducedSetoid α ≤ (F.inducedSetoid β).comap (F.P.map f) := by ...

public theorem inducedSetoid_unique (setoid : ∀ α : Type u, Setoid (F.P α))
    (mapsto : ∀ α β : Type u, ∀ f : α → β, setoid α ≤ (setoid β).comap (F.P.map f))
    (agrees : ∀ (α : Type u) (s : Set (ℕ ⊕ Sigma F.P.B)) (e : α ≃ s),
      setoid α = (F.setoid s).comap (F.P.map e))
    (α : Type u) : setoid α = F.inducedSetoid α := by ...
...
variable (F) (α) in
@[expose, coe]
public def Obj := Quotient (inducedSetoid F α)
...
variable (F) in
@[expose]
public def map : F α → F β :=
  Quotient.map (F.P.map f) (F.inducedSetoid_coherent f)

Next I do the fixpoint and cofixpoint of this polynomial functor F, and I run into a problem with the QPF.Fix.mk and QPF.Cofix.dest. Since fixpoint is implemented as a quotient of the W-type and polynomial functor (docs#PFunctor.Obj) is implemented as Σ x : P.A, P.B x → α, when we want to make the QPF.Fix.mk : F F.Fix → F.Fix we have to give a map (F.P.B i → Quotient ...) → Quotient ... and this requires the axiom of choice. The way that the current implementation gets around this is by giving for each Type u a section abs for the quotient map, so then abs is a choice function that can be used to choose quotient representatives without the axiom of choice. But I don't see how that's an option here since there's not a way to give the abs functions without quantifying over Type u and then we'll have QPF.{u, uA, uB} again.

The same kind of problem occurs when I attempted to define QPF.Cofix.dest. So I'm a bit stuck, until I find a way that lets it be computable and universe polymorphic.