diff --git a/Qpf/Builtins/List.lean b/Qpf/Builtins/List.lean
index 286b897..91dc5b5 100644
--- a/Qpf/Builtins/List.lean
+++ b/Qpf/Builtins/List.lean
@@ -10,22 +10,23 @@ import Mathlib.Tactic.FinCases
 namespace MvQPF
 namespace List
 
-  def ListPFunctor : MvPFunctor.{u} 1
-    := ⟨ULift Nat, fun n => !![PFin2 n.down]⟩
+  def ListPFunctor : MvPFunctor 1
+    := ⟨Nat, fun n => !![Fin2 n]⟩
 
+  #print ListPFunctor
 
   abbrev QpfList' := ListPFunctor.Obj
   abbrev List' := @TypeFun.ofCurried 1 List
 
   abbrev box {Γ} (x : List' Γ) : QpfList' Γ
     := ⟨
-        ULift.up x.length,
-        fun .fz j => Vec.ofList x (PFin2.toFin2 j)
+        x.length, 
+        fun .fz j => Vec.ofList x j
       ⟩
 
-  abbrev unbox {Γ} (x : QpfList' Γ) : List' Γ
-    := Vec.toList fun i => x.snd 0 (PFin2.ofFin2 i)
-
+  abbrev unbox {Γ} (x : QpfList' Γ) : List' Γ 
+    := Vec.toList fun i => x.snd 0 i
+    
   private theorem typeext {α} {f g : α → Sort _} (f_eq_g: f = g) :
     ((a : α) → f a) = ((a : α) → g a) :=
   by
@@ -38,8 +39,8 @@ namespace List
   instance : MvQPF List' :=
     .ofIsomorphism _ box unbox (
       by
-        intros Γ x
-        rcases x with ⟨⟨n⟩, v⟩
+        intros Γ x;
+        rcases x with ⟨n, v⟩
         dsimp[ListPFunctor] at v
         simp only [box, Fin2.instOfNatFin2HAddNatInstHAddInstAddNatOfNat, unbox]
 
@@ -60,7 +61,7 @@ namespace List
           · intro i
             fin_cases i
             apply HEq.trans Vec.ofList_toList_iso'
-            simp only [Eq.ndrec, id_eq, eq_mpr_eq_cast, PFin2.toFin2_ofFin2]
+            simp only [Eq.ndrec, id_eq, eq_mpr_eq_cast]
             apply HEq.trans cast_fun_arg
             rfl
 
@@ -70,7 +71,7 @@ namespace List
           fin_cases i
 
           simp only [ListPFunctor, TypeVec.Arrow, DVec];
-          have : List.length (unbox { fst := { down := n }, snd := v }) = n := by simp
+          have : List.length (unbox { fst := n, snd := v }) = n := by simp
           simp[this]
 
         case H₄ => intros; rfl
diff --git a/Qpf/Macro/Data.lean b/Qpf/Macro/Data.lean
index 680b1aa..afa1c29 100644
--- a/Qpf/Macro/Data.lean
+++ b/Qpf/Macro/Data.lean
@@ -20,9 +20,9 @@ private def Array.enum (as : Array α) : Array (Nat × α) :=
 
   The result corresponds to a `i : PFin2 _` such that `i.toNat == n`
 -/
-private def PFin2.quoteOfNat : Nat → Term
-  | 0   => mkIdent ``PFin2.fz
-  | n+1 => Syntax.mkApp (mkIdent ``PFin2.fs) #[(quoteOfNat n)]
+-- private def PFin2.quoteOfNat : Nat → Term
+--   | 0   => mkIdent ``PFin2.fz
+--   | n+1 => Syntax.mkApp (mkIdent ``PFin2.fs) #[(quoteOfNat n)]
 
 private def Fin2.quoteOfNat : Nat → Term
   | 0   => mkIdent ``Fin2.fz
@@ -168,7 +168,7 @@ def mkChildT (view : InductiveView) (r : Replace) (headTName : Name) : CommandEl
 
     let counts := countVarOccurences r ctor.type?
     let counts := counts.map fun n =>
-                    Syntax.mkApp (mkIdent ``PFin2) #[quote n]
+                    Syntax.mkApp (mkIdent ``Fin2) #[quote n]
 
     `(matchAltExpr| | $head => (!![ $counts,* ]))
 
@@ -236,11 +236,11 @@ def mkQpf (shapeView : InductiveView) (ctorArgs : Array CtorArgs) (headT P : Ide
             let i := arity - 1 - i
             let body ← if args.size == 0 then
                           -- `(fun j => Fin2.elim0 (C:=fun _ => _) j)
-                          `(PFin2.elim0)
+                          `(Fin2.elim0)
                         else
                           let alts ← args.enum.mapM fun (j, arg) =>
                               let arg := mkIdent arg
-                              `(matchAltExpr| | $(PFin2.quoteOfNat j) => $arg)
+                              `(matchAltExpr| | $(Fin2.quoteOfNat j) => $arg)
                           `(
                             fun j => match j with
                               $alts:matchAlt*
@@ -275,7 +275,7 @@ def mkQpf (shapeView : InductiveView) (ctorArgs : Array CtorArgs) (headT P : Ide
         ((t.indexOf? arg).map fun ⟨j, _⟩ => (i, j)).toList
       ).toList.join.get! 0
 
-      `($unbox_child $(Fin2.quoteOfNat i) $(PFin2.quoteOfNat j))
+      `($unbox_child $(Fin2.quoteOfNat i) $(Fin2.quoteOfNat j))
 
     let body := Syntax.mkApp alt args
 
@@ -303,7 +303,7 @@ def mkQpf (shapeView : InductiveView) (ctorArgs : Array CtorArgs) (headT P : Ide
         <;> simp
         <;> apply congrArg
         <;> (funext i; fin_cases i)
-        <;> (funext (j : PFin2 _); fin_cases j)
+        <;> (funext (j : Fin2 _); fin_cases j)
         <;> rfl
 
     instance $functor:ident : MvFunctor (@TypeFun.ofCurried $(quote arity) $shape) where
diff --git a/Qpf/MathlibPort/Fin2.lean b/Qpf/MathlibPort/Fin2.lean
index f64e9ef..5bba37a 100644
--- a/Qpf/MathlibPort/Fin2.lean
+++ b/Qpf/MathlibPort/Fin2.lean
@@ -33,92 +33,210 @@ different definitional equalities.
 
 open Nat
 
-universe u
-
-/-- An alternate definition of `fin n` defined as an inductive type instead of a subtype of `Nat`. -/
-inductive PFin2 : Nat → Type u
-  | /-- `0` as a member of `fin (succ n)` (`fin 0` is empty) -/
-  fz {n} : PFin2 (succ n)
-  | /-- `n` as a member of `fin (succ n)` -/
-  fs {n} : PFin2 n → PFin2 (succ n)
-  deriving DecidableEq
-
-namespace PFin2
-
-/-- Ex falso. The dependent eliminator for the empty `PFin2 0` type. -/
-def elim0 {C : PFin2 0 → Sort u} : ∀ i : PFin2 0, C i :=
-  by intro i; cases i
-
-/-- Converts a `PFin2` into a natural. -/
-def toNat : ∀ {n}, PFin2 n → Nat
-  | _, @fz _ => 0
-  | _, @fs _ i => succ (toNat i)
-
-/-- Shows that `toNat` produces a natural withing the range -/
-theorem toNat_lt (i : PFin2 n) :
-  i.toNat < n :=
-by
-  induction i
-  case fz       => apply succ_pos
-  case fs _ ih  => apply lt_succ_of_le ih
-
-/-- Converts a `PFin2` into the a `Fin` -/
-def toFin : PFin2 n → Fin n
-  := fun i => ⟨i.toNat, toNat_lt i⟩
-
-/-- Converts a natural into a `PFin2` given a proof that it is in range -/
-def ofNatLt : ∀ {n} (k : Nat) (_ : k < n), PFin2 n
-  | 0, _, h            => by contradiction
-  | succ n, 0, _       => fz
-  | succ n, succ k, h  => fs $ @ofNatLt n k (lt_of_succ_lt_succ h)
-
-
-/-- Converts a `Fin` into a `PFin2` -/
-def ofFin : Fin n → PFin2 n
-  := fun ⟨i, h⟩ => ofNatLt i h
-
-
-
-/-- This is a simple type class inference prover for proof obligations
-  of the form `m < n` where `m n : Nat`. -/
-class IsLt (m n : Nat) where
-  h : m < n
-
-instance IsLt.zero n : IsLt 0 (succ n) :=
-  ⟨succ_pos _⟩
-
-instance IsLt.succ m n [l : IsLt m n] : IsLt (succ m) (succ n) :=
-  ⟨succ_lt_succ l.h⟩
-
-/-- Use type class inference to infer the boundedness proof, so that we can directly convert a
-`nat` into a `PFin2 n`. This supports notation like `&1 : fin 3`. -/
-def ofNat' : ∀ {n} m [IsLt m n], PFin2 n
-  | 0, _, ⟨h⟩ => absurd h (Nat.not_lt_zero _)
-  | succ _, 0, ⟨_⟩ => fz
-  | succ n, succ m, ⟨h⟩ => fs (@ofNat' n m ⟨lt_of_succ_lt_succ h⟩)
-
-instance : Inhabited (PFin2 1) :=
-  ⟨fz⟩
+-- universe u
+--
+-- /-- An alternate definition of `fin n` defined as an inductive type instead of a subtype of `Nat`. -/
+-- inductive PFin2 : Nat → Type u
+--   | /-- `0` as a member of `fin (succ n)` (`fin 0` is empty) -/
+--   fz {n} : PFin2 (succ n)
+--   | /-- `n` as a member of `fin (succ n)` -/
+--   fs {n} : PFin2 n → PFin2 (succ n)
+--   deriving DecidableEq
+--
+-- namespace PFin2
+--
+-- /-- Ex falso. The dependent eliminator for the empty `PFin2 0` type. -/
+-- def elim0 {C : PFin2 0 → Sort u} : ∀ i : PFin2 0, C i :=
+--   by intro i; cases i
+--
+-- /-- Converts a `PFin2` into a natural. -/
+-- def toNat : ∀ {n}, PFin2 n → Nat
+--   | _, @fz _ => 0
+--   | _, @fs _ i => succ (toNat i)
+--
+-- /-- Shows that `toNat` produces a natural withing the range -/
+-- theorem toNat_lt (i : PFin2 n) :
+--   i.toNat < n :=
+-- by
+--   induction i
+--   case fz       => apply succ_pos
+--   case fs _ ih  => apply lt_succ_of_le ih
+--
+-- /-- Converts a `PFin2` into the a `Fin` -/
+-- def toFin : PFin2 n → Fin n
+--   := fun i => ⟨i.toNat, toNat_lt i⟩
+--
+-- /-- Converts a natural into a `PFin2` given a proof that it is in range -/
+-- def ofNatLt : ∀ {n} (k : Nat) (_ : k < n), PFin2 n
+--   | 0, _, h            => by contradiction
+--   | succ n, 0, _       => fz
+--   | succ n, succ k, h  => fs $ @ofNatLt n k (lt_of_succ_lt_succ h)
+--
+--
+-- /-- Converts a `Fin` into a `PFin2` -/
+-- def ofFin : Fin n → PFin2 n
+--   := fun ⟨i, h⟩ => ofNatLt i h
+--
+--
+--
+-- /-- This is a simple type class inference prover for proof obligations
+--   of the form `m < n` where `m n : Nat`. -/
+-- class IsLt (m n : Nat) where
+--   h : m < n
+--
+-- instance IsLt.zero n : IsLt 0 (succ n) :=
+--   ⟨succ_pos _⟩
+--
+-- instance IsLt.succ m n [l : IsLt m n] : IsLt (succ m) (succ n) :=
+--   ⟨succ_lt_succ l.h⟩
+--
+-- /-- Use type class inference to infer the boundedness proof, so that we can directly convert a
+-- `nat` into a `PFin2 n`. This supports notation like `&1 : fin 3`. -/
+-- def ofNat' : ∀ {n} m [IsLt m n], PFin2 n
+--   | 0, _, ⟨h⟩ => absurd h (Nat.not_lt_zero _)
+--   | succ _, 0, ⟨_⟩ => fz
+--   | succ n, succ m, ⟨h⟩ => fs (@ofNat' n m ⟨lt_of_succ_lt_succ h⟩)
+--
+-- instance : Inhabited (PFin2 1) :=
+--   ⟨fz⟩
+--
+--
+-- /--
+--   Weakens the bound on a `PFin2`, without changing the value
+-- -/
+-- def weaken : PFin2 n → PFin2 (succ n)
+--   | fz   => fz
+--   | fs k => fs $ weaken k
+--
+-- /--
+--   The maximal element of `PFin2 (n+1)`, i.e., `n`
+-- -/
+-- def last : {n : Nat} → PFin2 (n+1)
+--   | 0   => fz
+--   | n+1 => fs (@last n)
+--
+-- /--
+--   The inverse of `i` w.r.t. addition modulo `n`, i.e., .last - i
+-- -/
+-- def inv : {n : Nat} → PFin2.{u} n → PFin2.{u} n
+--   | 0,    _     => by contradiction
+--   | 1,    .fs _ => by contradiction
+--   | n+1,  .fz   => last
+--   | n+2,  .fs i => i.inv.weaken
+--
+-- theorem inv_last_eq_fz {n : Nat} :
+--   (@last n).inv = .fz :=
+-- by
+--   induction n <;> simp [inv, last, weaken, *]
+--
+-- theorem inv_weaken_eq_fs_inv {n : Nat} (i : PFin2 n):
+--   inv (weaken  i) = .fs (inv i) :=
+-- by
+--   induction i
+--   <;> simp[inv, weaken, last]
+--   case fs n i ih =>
+--     simp[ih]
+--     cases n
+--     . contradiction
+--     . simp[inv, weaken]
+--
+--
+-- @[simp]
+-- theorem inv_involution {i : PFin2 n} :
+--   i.inv.inv = i :=
+-- by
+--     induction i
+--     simp [inv]
+--     case fz => apply inv_last_eq_fz
+--     case fs n i ih => {
+--       cases n;
+--       case zero => contradiction
+--       case succ n =>
+--         simp[inv]
+--         rw[inv_weaken_eq_fs_inv i.inv]
+--         apply congrArg
+--         apply ih
+--     }
+--
+--
+--     -- case zero.fs => contradiction
+--     -- case succ.fs => simp[inv_last_eq_fz, weaken]
+--
+--
+-- /--
+--   Typeclass instances to make it easier to work with `PFin2`'s
+-- -/
+-- @[simp]
+-- instance (n : Nat) : OfNat (PFin2 (n+1)) (nat_lit 0) := ⟨fz⟩
+-- instance (n : Nat) : OfNat (PFin2 (n+2)) (nat_lit 1) := ⟨fs 0⟩
+-- instance (n : Nat) : OfNat (PFin2 (n+3)) (nat_lit 2) := ⟨fs 1⟩
+--
+-- def ofFin2 : Fin2 n → PFin2 n
+--   | .fz   => .fz
+--   | .fs i => .fs <| ofFin2 i
+--
+-- def toFin2 : PFin2 n → Fin2 n
+--   | .fz   => .fz
+--   | .fs i => .fs <| toFin2 i
+--
+-- @[simp]
+-- theorem ofFin2_toFin2_iso {i : Fin2 n} :
+--   (toFin2 <| ofFin2 i) = i :=
+-- by
+--   induction i
+--   . rfl
+--   . simp [ofFin2, toFin2, *]
+--
+-- @[simp]
+-- theorem toFin2_ofFin2_iso {i : PFin2 n} :
+--   (ofFin2 <| toFin2 i) = i :=
+-- by
+--   induction i
+--   . rfl
+--   . simp [ofFin2, toFin2, *]
+--
+-- instance : Coe (Fin2 n) (PFin2 n) := ⟨ofFin2⟩
+-- instance : Coe (PFin2 n) (Fin2 n) := ⟨toFin2⟩
+--
+-- instance : Coe (PFin2 n) (Fin n) := ⟨toFin⟩
+-- instance : Coe (Fin n) (PFin2 n) := ⟨ofFin⟩
+--
+-- instance : Coe (Fin n) (Fin2 n) := ⟨fun i => toFin2 <| ofFin.{0} i⟩
+-- instance : Coe (Fin2 n) (Fin n) := ⟨fun i => toFin <| ofFin2.{0} i⟩
+--
+-- end PFin2
+--
+--
+namespace Fin2
+  /--
+  Typeclass instances to make it easier to work with `PFin2`'s
+-/
+@[simp]
+instance (n : Nat) : OfNat (Fin2 (n+1)) (nat_lit 0) := ⟨fz⟩
+instance (n : Nat) : OfNat (Fin2 (n+2)) (nat_lit 1) := ⟨fs 0⟩
+instance (n : Nat) : OfNat (Fin2 (n+3)) (nat_lit 2) := ⟨fs 1⟩
 
+-- def inv : Fin2 n → Fin2 n
+--   := fun i => (PFin2.inv.{0} i : PFin2 n)
 
 /--
   Weakens the bound on a `PFin2`, without changing the value
 -/
-def weaken : PFin2 n → PFin2 (succ n)
+def weaken : Fin2 n → Fin2 (succ n)
   | fz   => fz
   | fs k => fs $ weaken k
 
 /--
   The maximal element of `PFin2 (n+1)`, i.e., `n`
 -/
-def last : {n : Nat} → PFin2 (n+1)
+def last : {n : Nat} → Fin2 (n+1)
   | 0   => fz
   | n+1 => fs (@last n)
 
 /--
   The inverse of `i` w.r.t. addition modulo `n`, i.e., .last - i
 -/
-def inv : {n : Nat} → PFin2.{u} n → PFin2.{u} n
+def inv : {n : Nat} → Fin2 n → Fin2 n
   | 0,    _     => by contradiction
   | 1,    .fs _ => by contradiction
   | n+1,  .fz   => last
@@ -129,7 +247,7 @@ theorem inv_last_eq_fz {n : Nat} :
 by
   induction n <;> simp [inv, last, weaken, *]
 
-theorem inv_weaken_eq_fs_inv {n : Nat} (i : PFin2 n):
+theorem inv_weaken_eq_fs_inv {n : Nat} (i : Fin2 n):
   inv (weaken  i) = .fs (inv i) :=
 by
   induction i
@@ -140,9 +258,8 @@ by
     . contradiction
     . simp[inv, weaken]
 
-
 @[simp]
-theorem inv_involution {i : PFin2 n} :
+theorem inv_involution {i : Fin2 n} :
   i.inv.inv = i :=
 by
     induction i
@@ -158,74 +275,30 @@ by
         apply ih
     }
 
+/-- Shows that `toNat` produces a natural withing the range -/
+theorem toNat_lt (i : Fin2 n) :
+  i.toNat < n :=
+by
+  induction i
+  case fz       => apply succ_pos
+  case fs _ ih  => apply lt_succ_of_le ih
 
-    -- case zero.fs => contradiction
-    -- case succ.fs => simp[inv_last_eq_fz, weaken]
-
-
-/--
-  Typeclass instances to make it easier to work with `PFin2`'s
--/
-@[simp]
-instance (n : Nat) : OfNat (PFin2 (n+1)) (nat_lit 0) := ⟨fz⟩
-instance (n : Nat) : OfNat (PFin2 (n+2)) (nat_lit 1) := ⟨fs 0⟩
-instance (n : Nat) : OfNat (PFin2 (n+3)) (nat_lit 2) := ⟨fs 1⟩
-
-def ofFin2 : Fin2 n → PFin2 n
-  | .fz   => .fz
-  | .fs i => .fs <| ofFin2 i
-
-def toFin2 : PFin2 n → Fin2 n
-  | .fz   => .fz
-  | .fs i => .fs <| toFin2 i
-
-@[simp] theorem ofFin2_toFin2 (i : Fin2 n) :
-    (toFin2 <| ofFin2 i) = i := by
-  induction i <;> simp [ofFin2, toFin2, *]
-
-@[simp] theorem toFin2_ofFin2 (i : PFin2 n) :
-    (ofFin2 <| toFin2 i) = i := by
-  induction i <;> simp [ofFin2, toFin2, *]
-
-def equivFin2 (n : Nat) : PFin2 n ≃ Fin2 n where
-  toFun     := toFin2
-  invFun    := ofFin2
-  left_inv  := toFin2_ofFin2
-  right_inv := ofFin2_toFin2
-
-instance : Coe (Fin2 n) (PFin2 n) := ⟨ofFin2⟩
-instance : Coe (PFin2 n) (Fin2 n) := ⟨toFin2⟩
-
-instance : Coe (PFin2 n) (Fin n) := ⟨toFin⟩
-instance : Coe (Fin n) (PFin2 n) := ⟨ofFin⟩
-
-instance : Coe (Fin n) (Fin2 n) := ⟨fun i => toFin2 <| ofFin.{0} i⟩
-instance : Coe (Fin2 n) (Fin n) := ⟨fun i => toFin <| ofFin2.{0} i⟩
-
-instance : Fintype (PFin2 n) := Fintype.ofEquiv _ (equivFin2 n).symm
-
-@[simp] theorem ofFin2_eq (i : Fin2 n) : ofFin2 i = (equivFin2 _).symm i := rfl
-@[simp] theorem toFin2_eq (i : PFin2 n) : toFin2 i = (equivFin2 _) i := rfl
-
-@[simp] theorem toFin2_fz : (equivFin2 (n+1)) PFin2.fz = Fin2.fz                    := rfl
-@[simp] theorem toFin2_fs : (equivFin2 _) (PFin2.fs i) = Fin2.fs ((equivFin2 _) i)  := rfl
-
-@[simp] theorem ofFin2_fz : (equivFin2 (n+1)).symm Fin2.fz = PFin2.fz                         := rfl
-@[simp] theorem ofFin2_fs : (equivFin2 _).symm (Fin2.fs i) = PFin2.fs ((equivFin2 _).symm i)  := rfl
+/-- Converts a `PFin2` into the a `Fin` -/
+def toFin : Fin2 n → Fin n
+  := fun i => ⟨i.toNat, toNat_lt i⟩
 
-end PFin2
+/-- Converts a natural into a `PFin2` given a proof that it is in range -/
+def ofNatLt : ∀ {n} (k : Nat) (_ : k < n), Fin2 n
+  | 0, _, h            => by contradiction
+  | succ n, 0, _       => fz
+  | succ n, succ k, h  => fs $ @ofNatLt n k (lt_of_succ_lt_succ h)
 
 
-namespace Fin2
-  /--
-  Typeclass instances to make it easier to work with `PFin2`'s
--/
-@[simp]
-instance (n : Nat) : OfNat (Fin2 (n+1)) (nat_lit 0) := ⟨fz⟩
-instance (n : Nat) : OfNat (Fin2 (n+2)) (nat_lit 1) := ⟨fs 0⟩
-instance (n : Nat) : OfNat (Fin2 (n+3)) (nat_lit 2) := ⟨fs 1⟩
+/-- Converts a `Fin` into a `PFin2` -/
+def ofFin : Fin n → Fin2 n
+  := fun ⟨i, h⟩ => ofNatLt i h
 
-def inv : Fin2 n → Fin2 n
-  := fun i => (PFin2.inv.{0} i : PFin2 n)
+instance : Coe (Fin n) (Fin2 n) := ⟨fun i => ofFin i⟩
+instance : Coe (Fin2 n) (Fin n) := ⟨fun i => toFin i⟩
 
 end Fin2
diff --git a/Qpf/PFunctor/Multivariate/Constructions/Prod.lean b/Qpf/PFunctor/Multivariate/Constructions/Prod.lean
index a10d949..e6aaf2b 100644
--- a/Qpf/PFunctor/Multivariate/Constructions/Prod.lean
+++ b/Qpf/PFunctor/Multivariate/Constructions/Prod.lean
@@ -11,11 +11,11 @@ import Qpf.Qpf.Multivariate.Basic
 namespace MvQPF
 namespace Prod
 
-open PFin2 (fz fs)
-
-def P : MvPFunctor 2
-  := .mk Unit fun _ _ => PFin2 1
+open Fin2 (fz fs)
 
+def P : MvPFunctor 2 
+  := .mk Unit fun _ _ => Fin2 1
+  
 
 abbrev QpfProd' := P.Obj
 abbrev QpfProd  := TypeFun.curried QpfProd'
@@ -47,7 +47,7 @@ def equiv {Γ} : Prod' Γ ≃ QpfProd' Γ := {
     rcases x with ⟨⟨⟩, f⟩;
     simp[mk];
     apply congrArg;
-    funext i (j : PFin2 _)
+    funext i (j : Fin2 _)
     fin_cases j
     fin_cases i
     <;> rfl
diff --git a/Qpf/PFunctor/Multivariate/Constructions/Sum.lean b/Qpf/PFunctor/Multivariate/Constructions/Sum.lean
index 01a7f74..d4e6ab2 100644
--- a/Qpf/PFunctor/Multivariate/Constructions/Sum.lean
+++ b/Qpf/PFunctor/Multivariate/Constructions/Sum.lean
@@ -11,28 +11,29 @@ import Qpf.Qpf.Multivariate.Basic
 namespace MvQPF
 namespace Sum
 
-universe u
+-- universe u
 
-def SumPFunctor : MvPFunctor.{u} 2
-  := ⟨PFin2 2,
-      fun
-      | 0 => !![PFin2 1, PFin2 0] -- inl
-      | 1 => !![PFin2 0, PFin2 1] -- inr
+def SumPFunctor : MvPFunctor 2
+  := ⟨Fin2 2, 
+      fun 
+      | 0 => !![Fin2 1, Fin2 0] -- inl
+      | 1 => !![Fin2 0, Fin2 1] -- inr
     ⟩
 
+#check SumPFunctor
 
 abbrev QpfSum' := SumPFunctor.Obj
 abbrev QpfSum  := TypeFun.curried QpfSum'
 
 def inl {Γ : TypeVec 2} (a : Γ 1) : QpfSum' Γ
-  := ⟨PFin2.ofNat' 0,
-      fun
+  := ⟨Fin2.ofNat' 0, 
+      fun 
       | 1, _ => a
     ⟩
 
 def inr {Γ : TypeVec 2} (b : Γ 0) : QpfSum' Γ
-  := ⟨PFin2.ofNat' 1,
-      fun
+  := ⟨Fin2.ofNat' 1, 
+      fun 
       | 0, _ => b
       | 1, x => by cases x
     ⟩
@@ -56,13 +57,12 @@ def equiv {Γ} : Sum' Γ ≃ QpfSum' Γ :=
   left_inv  := by intro x; cases x <;> rfl
   right_inv := by
     intro x
-    rcases x with ⟨(i : PFin2 _), f⟩
+    rcases x with ⟨(i : Fin2 _), f⟩
     dsimp only [box, unbox, inl, inr]
     fin_cases i <;> {
-      simp only [Function.Embedding.coeFn_mk, PFin2.ofFin2_fs, PFin2.ofFin2_fz,
-        Fin2.instOfNatFin2HAddNatInstHAddInstAddNatOfNat, Nat.rec_zero]
+      simp only [Function.Embedding.coeFn_mk, Fin2.instOfNatFin2HAddNatInstHAddInstAddNatOfNat, Nat.rec_zero]
       apply congrArg
-      funext i; fin_cases i <;> (funext (j : PFin2 _); fin_cases j)
+      funext i; fin_cases i <;> (funext (j : Fin2 _); fin_cases j)
       rfl
     }
 }
diff --git a/Qpf/Util/Vec.lean b/Qpf/Util/Vec.lean
index f0da060..3f972bd 100644
--- a/Qpf/Util/Vec.lean
+++ b/Qpf/Util/Vec.lean
@@ -75,7 +75,7 @@ macro_rules
 
 
 namespace Vec
-  theorem drop_append1 {v : Vec α n} {a : α} {i : PFin2 n} :
+  theorem drop_append1 {v : Vec α n} {a : α} {i : Fin2 n} :
       drop (append1 v a) i = v i :=
     rfl
 
@@ -104,7 +104,7 @@ namespace Vec
     funext i;
     dsimp only [reverse]
     apply congrArg;
-    simp only [Fin2.inv, PFin2.toFin2_ofFin2, PFin2.inv_involution, PFin2.ofFin2_toFin2]
+    simp only [Fin2.inv, Fin2.inv_involution]
 end Vec
 
 
@@ -178,8 +178,8 @@ namespace Vec
       }
 
   theorem ofList_toList_iso' {v : Vec α n} :
-    HEq (fun (j : PFin2.{u} (toList v).length) => ofList (toList v) j.toFin2)
-        (fun (j : PFin2.{u} (toList v).length) => v <| PFin2.toFin2 <| cast (by rw[toList_length_eq_n]) j) :=
+    HEq (fun (j : Fin2 (toList v).length) => ofList (toList v) j)
+        (fun (j : Fin2 (toList v).length) => v <| cast (by rw[toList_length_eq_n]) j) :=
   by
     apply HEq.funext
     . rfl
@@ -187,9 +187,10 @@ namespace Vec
     have n_eq : (toList v).length = n := toList_length_eq_n;
     apply hcongr
     . apply ofList_toList_iso
-    . intros
-      apply hcongr <;> intros <;> (try rw[n_eq])
-      . simp_heq
+    . simp_heq 
+      -- intros
+      -- apply hcongr <;> intros <;> (try rw[n_eq])
+      -- . simp_heq
     . intros; simp
     . rw[n_eq]
 
diff --git a/Test/Comp.lean b/Test/Comp.lean
index 036215c..76f0679 100644
--- a/Test/Comp.lean
+++ b/Test/Comp.lean
@@ -12,6 +12,6 @@ qpf P₁ α β := α
 qpf P₂ α β := β
 
 qpf C₁ α β := Nat
-qpf C₂ (n : Nat) α β := PFin2 n
+qpf C₂ (n : Nat) α β := Fin2 n
 
-qpf G₄ α β ρ := QpfList ρ
\ No newline at end of file
+qpf G₄ α β ρ := QpfList ρ
diff --git a/Test/Dead.lean b/Test/Dead.lean
index c22667d..8fd1b9e 100644
--- a/Test/Dead.lean
+++ b/Test/Dead.lean
@@ -7,11 +7,11 @@ import Qpf
 
 
 codata FinAlt {n : Nat} β
-  | mk : PFin2 n → FinAlt β
+  | mk : Fin2 n → FinAlt β
 
 #print FinAlt.mk
 
 
 data QpfList₄ (dead : Type) β γ where
   | nil   : QpfList₄ dead β γ
-  | cons  : QpfList₄ dead β γ → QpfList₄ dead β γ
\ No newline at end of file
+  | cons  : QpfList₄ dead β γ → QpfList₄ dead β γ
diff --git a/Test/List.lean b/Test/List.lean
index 027b487..add4502 100644
--- a/Test/List.lean
+++ b/Test/List.lean
@@ -6,4 +6,4 @@ data QpfList α
   | nil
   | cons : α → QpfList α → QpfList α   
 
-end Test
\ No newline at end of file
+end Test