From 2a6eaadaf00436317d5ca4a31b755dab9e3a5981 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 4 Dec 2024 15:05:17 +0000
Subject: [PATCH 1/4] fix: remove `MvFunctor` instance arg from `IsPolynomial`

The instance is already bundled into MvQPF
---
 Qpf/Qpf/Multivariate/Basic.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Qpf/Qpf/Multivariate/Basic.lean b/Qpf/Qpf/Multivariate/Basic.lean
index 81318bc..f235665 100644
--- a/Qpf/Qpf/Multivariate/Basic.lean
+++ b/Qpf/Qpf/Multivariate/Basic.lean
@@ -7,7 +7,7 @@ namespace MvQPF
     `repr_abs` is the last property needed to show that `abs` is an isomorphism, with `repr`
     its inverse
   -/
-  class IsPolynomial {n} (F : TypeVec n → Type _) [MvFunctor F] extends MvQPF F where
+  class IsPolynomial {n} (F : TypeVec n → Type _) extends MvQPF F where
     repr_abs : ∀ {α} (x : P.Obj α), repr (abs x) = x
 
 
@@ -83,6 +83,5 @@ namespace MvQPF
     apply cast ?_ p
     congr
     · rw [TypeFun.ofCurried_curried_involution]
-    · exact HEq.symm (eqRec_heq ..)
 
 end MvQPF

From 9e1ae07b21b48f3d494d8ea841c8508782dabe72 Mon Sep 17 00:00:00 2001
From: Max Nowak <max.nowak.j@gmail.com>
Date: Tue, 3 Dec 2024 10:37:02 -0800
Subject: [PATCH 2/4] fix: make `Prod'` universe-polymorphic

---
 Qpf/PFunctor/Multivariate/Constructions/Prod.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Qpf/PFunctor/Multivariate/Constructions/Prod.lean b/Qpf/PFunctor/Multivariate/Constructions/Prod.lean
index a10d949..9761d3a 100644
--- a/Qpf/PFunctor/Multivariate/Constructions/Prod.lean
+++ b/Qpf/PFunctor/Multivariate/Constructions/Prod.lean
@@ -13,8 +13,8 @@ namespace Prod
 
 open PFin2 (fz fs)
 
-def P : MvPFunctor 2
-  := .mk Unit fun _ _ => PFin2 1
+def P : MvPFunctor.{u} 2
+  := .mk PUnit fun _ _ => PFin2 1
 
 
 abbrev QpfProd' := P.Obj
@@ -30,9 +30,9 @@ abbrev Prod' : TypeFun 2
 /--
   Constructor for `QpfProd'`
 -/
-def mk (a : Γ 1) (b : Γ 0) : QpfProd' Γ
+def mk (a : Γ 1) (b : Γ 0) : QpfProd'.{u} Γ
   := ⟨
-      (),
+      ⟨⟩,
       fun
       | 1, _ => a
       | 0, _ => b

From 9cfc50cfa0dc561f5b7a1bf08e693b2a52172383 Mon Sep 17 00:00:00 2001
From: Max Nowak <max.nowak.j@gmail.com>
Date: Tue, 3 Dec 2024 13:46:12 -0800
Subject: [PATCH 3/4] Make Arrow universe-polymorphic

---
 Qpf/PFunctor/Multivariate/Constructions/Arrow.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Qpf/PFunctor/Multivariate/Constructions/Arrow.lean b/Qpf/PFunctor/Multivariate/Constructions/Arrow.lean
index 6e535a7..ce9d4be 100644
--- a/Qpf/PFunctor/Multivariate/Constructions/Arrow.lean
+++ b/Qpf/PFunctor/Multivariate/Constructions/Arrow.lean
@@ -36,8 +36,8 @@ namespace Arrow
 
 
 
-  def box (f : Arrow' α Γ) : (QpfArrow' α Γ)
-    := ⟨(), fun | 0 => f⟩
+  def box (f : Arrow'.{u} α Γ) : (QpfArrow' α Γ)
+    := ⟨⟨⟩, fun | 0 => f⟩
 
   def unbox : QpfArrow' α Γ → Arrow' α Γ
     | ⟨_, f⟩ => f 0
@@ -60,7 +60,7 @@ namespace Arrow
   instance : MvFunctor (Arrow' x) where
     map f a     := unbox <| (ArrowPFunctor x).map f <| box a
 
-  instance : MvQPF (Arrow' x) where
+  instance instMvQPF : MvQPF (Arrow' x) where
     P           := ArrowPFunctor x
     abs         := @unbox x
     repr        := @box x

From 25859286f93cbc4c31c656b6399ec39d4b3d54b8 Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 4 Dec 2024 15:16:36 +0000
Subject: [PATCH 4/4] Apply suggestions from code review

---
 Qpf/PFunctor/Multivariate/Constructions/Prod.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Qpf/PFunctor/Multivariate/Constructions/Prod.lean b/Qpf/PFunctor/Multivariate/Constructions/Prod.lean
index 9761d3a..0c36363 100644
--- a/Qpf/PFunctor/Multivariate/Constructions/Prod.lean
+++ b/Qpf/PFunctor/Multivariate/Constructions/Prod.lean
@@ -13,8 +13,8 @@ namespace Prod
 
 open PFin2 (fz fs)
 
-def P : MvPFunctor.{u} 2
-  := .mk PUnit fun _ _ => PFin2 1
+def P : MvPFunctor.{u} 2 := 
+  .mk PUnit fun _ _ => PFin2 1
 
 
 abbrev QpfProd' := P.Obj
@@ -30,8 +30,8 @@ abbrev Prod' : TypeFun 2
 /--
   Constructor for `QpfProd'`
 -/
-def mk (a : Γ 1) (b : Γ 0) : QpfProd'.{u} Γ
-  := ⟨
+def mk (a : Γ 1) (b : Γ 0) : QpfProd'.{u} Γ := 
+  ⟨
       ⟨⟩,
       fun
       | 1, _ => a