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
diff --git a/Qpf/PFunctor/Multivariate/Constructions/Prod.lean b/Qpf/PFunctor/Multivariate/Constructions/Prod.lean
index a42097c..91ee803 100644
--- a/Qpf/PFunctor/Multivariate/Constructions/Prod.lean
+++ b/Qpf/PFunctor/Multivariate/Constructions/Prod.lean
@@ -12,8 +12,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
@@ -23,10 +23,11 @@ abbrev QpfProd  := TypeFun.curried QpfProd'
 def Prod' : TypeFun 2 :=
   @TypeFun.ofCurried 2 Prod
 
+
 /-- Constructor for `QpfProd'` -/
-def mk (a : Γ 1) (b : Γ 0) : QpfProd' Γ
-  := ⟨
-      (),
+def mk (a : Γ 1) (b : Γ 0) : QpfProd'.{u} Γ :=
+  ⟨
+      ⟨⟩,
       fun
       | 1, _ => a
       | 0, _ => b