From 58449e12b97e1c7886c8ba2a379d08b3ccd8168c 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 1/3] 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 67e99ac5339969f1fe220100c3c5f05ea37e20f9 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 2/3] 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 82b77ded81af2bd64005e798d6a1fbb971c3aefe Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Wed, 4 Dec 2024 15:16:36 +0000
Subject: [PATCH 3/3] 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