Remove PFin2 (without universe polymorphism)

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

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