diff --git a/Poly.lean b/Poly.lean
index b286754..3ee25a8 100644
--- a/Poly.lean
+++ b/Poly.lean
@@ -5,6 +5,5 @@ import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Presheaf
 -- import Poly.LCCC.BeckChevalley
 -- import Poly.LCCC.Presheaf
 -- import Poly.Type.Univariate
--- import Poly.Basic
 -- import Poly.Exponentiable
-import Poly.UvPoly
+import Poly.UvPoly.Basic
diff --git a/Poly/Bifunctor/Basic.lean b/Poly/Bifunctor/Basic.lean
new file mode 100644
index 0000000..3ca5ab0
--- /dev/null
+++ b/Poly/Bifunctor/Basic.lean
@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2025 Wojciech Nawrocki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Nawrocki
+-/
+import Mathlib.CategoryTheory.Adjunction.Basic
+
+import Poly.ForMathlib.CategoryTheory.NatIso
+import Poly.ForMathlib.CategoryTheory.Types
+
+/-! ## Composition of bifunctors -/
+
+namespace CategoryTheory.Functor
+
+variable {𝒞 𝒟' 𝒟 ℰ : Type*} [Category 𝒞] [Category 𝒟'] [Category 𝒟] [Category ℰ]
+
+/-- Precompose a bifunctor in the second argument.
+Note that `G ⋙₂ F ⋙ P = F ⋙ G ⋙₂ P` definitionally. -/
+@[simps]
+def comp₂ (F : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) : 𝒞 ⥤ 𝒟' ⥤ ℰ where
+  obj Γ := F ⋙ P.obj Γ
+  map f := whiskerLeft F (P.map f)
+
+@[inherit_doc]
+scoped [CategoryTheory] infixr:80 " ⋙₂ " => Functor.comp₂
+
+@[simp]
+theorem comp_comp₂ {𝒟'' : Type*} [Category 𝒟'']
+    (F : 𝒟'' ⥤ 𝒟') (G : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) :
+    (F ⋙ G) ⋙₂ P = F ⋙₂ (G ⋙₂ P) := by
+  rfl
+
+/-- Composition with `F,G` ordered like the arguments of `P` is considered `simp`ler. -/
+@[simp]
+theorem comp₂_comp {𝒞' : Type*} [Category 𝒞']
+    (F : 𝒞' ⥤ 𝒞) (G : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) :
+    G ⋙₂ (F ⋙ P) = F ⋙ (G ⋙₂ P) := by
+  rfl
+
+@[simps!]
+def comp₂_iso {F₁ F₂ : 𝒟' ⥤ 𝒟} {P₁ P₂ : 𝒞 ⥤ 𝒟 ⥤ ℰ}
+    (i : F₁ ≅ F₂) (j : P₁ ≅ P₂) : F₁ ⋙₂ P₁ ≅ F₂ ⋙₂ P₂ :=
+  NatIso.ofComponents₂ (fun C D => (j.app C).app (F₁.obj D) ≪≫ (P₂.obj C).mapIso (i.app D))
+    (fun _ _ => by simp [NatTrans.naturality_app_assoc])
+    (fun C f => by
+      have := congr_arg (P₂.obj C).map (i.hom.naturality f)
+      simp only [map_comp] at this
+      simp [this])
+
+@[simps!]
+def comp₂_isoWhiskerLeft {P₁ P₂ : 𝒞 ⥤ 𝒟 ⥤ ℰ} (F : 𝒟' ⥤ 𝒟) (i : P₁ ≅ P₂) :
+    F ⋙₂ P₁ ≅ F ⋙₂ P₂ :=
+  comp₂_iso (Iso.refl F) i
+
+@[simps!]
+def comp₂_isoWhiskerRight {F₁ F₂ : 𝒟' ⥤ 𝒟} (i : F₁ ≅ F₂) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) :
+    F₁ ⋙₂ P ≅ F₂ ⋙₂ P :=
+  comp₂_iso i (Iso.refl P)
+
+end CategoryTheory.Functor
+
+/-! ## Natural isomorphisms of bifunctors -/
+
+namespace CategoryTheory
+universe v u
+variable {𝒞 : Type u} [Category.{v} 𝒞]
+variable {𝒟 : Type*} [Category 𝒟]
+
+namespace coyoneda
+
+theorem comp₂_naturality₂_left (F : 𝒟 ⥤ 𝒞) (P : 𝒞ᵒᵖ ⥤ 𝒟 ⥤ Type v)
+    (i : F ⋙₂ coyoneda (C := 𝒞) ⟶ P) (X Y : 𝒞) (Z : 𝒟) (f : X ⟶ Y) (g : Y ⟶ F.obj Z) :
+    -- The `op`s really are a pain. Why can't they be definitional like in Lean 3 :(
+    (i.app <| .op X).app Z (f ≫ g) = (P.map f.op).app Z ((i.app <| .op Y).app Z g) := by
+  simp [← FunctorToTypes.naturality₂_left]
+
+theorem comp₂_naturality₂_right (F : 𝒟 ⥤ 𝒞) (P : 𝒞ᵒᵖ ⥤ 𝒟 ⥤ Type v)
+    (i : F ⋙₂ coyoneda (C := 𝒞) ⟶ P) (X : 𝒞) (Y Z : 𝒟) (f : X ⟶ F.obj Y) (g : Y ⟶ Z) :
+    (i.app <| .op X).app Z (f ≫ F.map g) = (P.obj <| .op X).map g ((i.app <| .op X).app Y f) := by
+  simp [← FunctorToTypes.naturality₂_right]
+
+end coyoneda
+
+namespace Adjunction
+
+variable {𝒟 : Type*} [Category 𝒟]
+
+/-- For `F ⊣ G`, `𝒟(FX, Y) ≅ 𝒞(X, GY)`. -/
+def coyoneda_iso {F : 𝒞 ⥤ 𝒟} {G : 𝒟 ⥤ 𝒞} (A : F ⊣ G) :
+    F.op ⋙ coyoneda (C := 𝒟) ≅ G ⋙₂ coyoneda (C := 𝒞) :=
+  NatIso.ofComponents₂ (fun C D => Equiv.toIso <| A.homEquiv C.unop D)
+    (fun _ _ => by ext : 1; simp [A.homEquiv_naturality_left])
+    (fun _ _ => by ext : 1; simp [A.homEquiv_naturality_right])
+
+end Adjunction
+end CategoryTheory
diff --git a/Poly/Bifunctor/Sigma.lean b/Poly/Bifunctor/Sigma.lean
new file mode 100644
index 0000000..6740cb5
--- /dev/null
+++ b/Poly/Bifunctor/Sigma.lean
@@ -0,0 +1,182 @@
+/-
+Copyright (c) 2025 Wojciech Nawrocki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Nawrocki
+-/
+import Mathlib.CategoryTheory.Comma.Over.Basic
+import Mathlib.CategoryTheory.Functor.Currying
+
+import SEq.Tactic.DepRewrite
+
+import Poly.ForMathlib.CategoryTheory.Elements
+import Poly.ForMathlib.CategoryTheory.Comma.Over.Basic
+import Poly.Bifunctor.Basic
+
+/-! ## Dependent sums of functors -/
+
+namespace CategoryTheory.Functor
+
+universe w v u t s r
+
+variable {𝒞 : Type t} [Category.{u} 𝒞] {𝒟 : Type r} [Category.{s} 𝒟]
+
+/-- Given functors `F : 𝒞 ⥤ Type v` and `G : ∫F ⥤ 𝒟 ⥤ Type v`,
+produce the functor `(C, D) ↦ (a : F(C)) × G((C, a))(D)`.
+
+This is a dependent sum that varies naturally
+in a parameter `C` of the first component,
+and a parameter `D` of the second component.
+
+We use this to package and compose natural equivalences
+where one side (or both) is a dependent sum, e.g.
+```
+H(C) ⟶ I(D)
+=========================
+(a : F(C)) × (G(C, a)(D))
+```
+is a natural isomorphism of bifunctors `𝒞ᵒᵖ ⥤ 𝒟 ⥤ Type v`
+given by `(C, D) ↦ H(C) ⟶ I(D)` and `G.Sigma`. -/
+@[simps!]
+/- Q: Is it necessary to special-case bifunctors?
+(1) General case `G : F.Elements ⥤ Type v` needs
+a functor `F'` s.t. `F'.Elements ≅ F.Elements × 𝒟`; very awkward.
+(2) General case `F : 𝒞 ⥤ 𝒟`, `G : ∫F ⥤ 𝒟`:
+- what conditions are needed on `𝒟` for `∫F` to make sense?
+- what about for `ΣF. G : 𝒞 ⥤ 𝒟` to make sense?
+- known concrete instances are `𝒟 ∈ {Type, Cat, Grpd}` -/
+def Sigma {F : 𝒞 ⥤ Type w} (G : F.Elements ⥤ 𝒟 ⥤ Type v) : 𝒞 ⥤ 𝒟 ⥤ Type (max w v) := by
+  refine curry.obj {
+    obj := fun (C, D) => (a : F.obj C) × (G.obj ⟨C, a⟩).obj D
+    map := fun (f, g) ⟨a, b⟩ =>
+      ⟨F.map f a, (G.map ⟨f, rfl⟩).app _ ((G.obj ⟨_, a⟩).map g b)⟩
+    map_id := ?_
+    map_comp := ?_
+  } <;> {
+    intros
+    ext ⟨a, b⟩ : 1
+    dsimp
+    congr! 1 with h
+    . simp
+    . rw! [h]; simp [FunctorToTypes.naturality]
+  }
+
+def Sigma.isoCongrLeft {F₁ F₂ : 𝒞 ⥤ Type w}
+    /- Q: What kind of map `F₂.Elements ⥤ F₁.Elements`
+    could `NatTrans.mapElements i.hom` generalize to?
+    We need to send `x ∈ F₂(C)` to something in `F₁(C)`;
+    so maybe the map has to at least be over `𝒞`. -/
+    (G : F₁.Elements ⥤ 𝒟 ⥤ Type v) (i : F₂ ≅ F₁) :
+    Sigma (NatTrans.mapElements i.hom ⋙ G) ≅ Sigma G := by
+  refine NatIso.ofComponents₂
+    (fun C D => Equiv.toIso {
+      toFun := fun ⟨a, b⟩ => ⟨i.hom.app C a, b⟩
+      invFun := fun ⟨a, b⟩ => ⟨i.inv.app C a, cast (by simp) b⟩
+      left_inv := fun ⟨_, _⟩ => by simp
+      right_inv := fun ⟨_, _⟩ => by simp
+    }) ?_ ?_ <;> {
+      intros
+      ext : 1
+      dsimp
+      apply have h := ?_; Sigma.ext h ?_
+      . simp [FunctorToTypes.naturality]
+      . dsimp [Sigma] at h ⊢
+        rw! [← h]
+        simp [NatTrans.mapElements]
+    }
+
+def Sigma.isoCongrRight {F : 𝒞 ⥤ Type w} {G₁ G₂ : F.Elements ⥤ 𝒟 ⥤ Type v} (i : G₁ ≅ G₂) :
+    Sigma G₁ ≅ Sigma G₂ := by
+  refine NatIso.ofComponents₂
+    (fun C D => Equiv.toIso {
+      toFun := fun ⟨a, b⟩ => ⟨a, (i.hom.app ⟨C, a⟩).app D b⟩
+      invFun := fun ⟨a, b⟩ => ⟨a, (i.inv.app ⟨C, a⟩).app D b⟩
+      left_inv := fun ⟨_, _⟩ => by simp
+      right_inv := fun ⟨_, _⟩ => by simp
+    }) ?_ ?_ <;> {
+      intros
+      ext : 1
+      dsimp
+      apply have h := ?_; Sigma.ext h ?_
+      . simp
+      . dsimp [Sigma] at h ⊢
+        simp [FunctorToTypes.naturality₂_left, FunctorToTypes.naturality₂_right]
+    }
+
+theorem comp₂_Sigma {𝒟' : Type*} [Category 𝒟']
+    {F : 𝒞 ⥤ Type w} (G : 𝒟' ⥤ 𝒟) (P : F.Elements ⥤ 𝒟 ⥤ Type v) :
+    G ⋙₂ Sigma P = Sigma (G ⋙₂ P) := by
+  apply Functor.hext
+  . intro C
+    apply Functor.hext
+    . intro; simp
+    . intros
+      apply heq_of_eq
+      ext : 1
+      apply Sigma.ext <;> simp
+  . intros
+    apply heq_of_eq
+    ext : 3
+    apply Sigma.ext <;> simp
+
+end CategoryTheory.Functor
+
+/-! ## Over categories -/
+
+namespace CategoryTheory.Over
+
+universe v u
+variable {𝒞 : Type u} [Category.{v} 𝒞]
+
+-- Q: is this in mathlib?
+@[simps]
+def equiv_Sigma {A : 𝒞} (X : 𝒞) (U : Over A) : (X ⟶ U.left) ≃ (b : X ⟶ A) × (Over.mk b ⟶ U) where
+  toFun g := ⟨g ≫ U.hom, Over.homMk g rfl⟩
+  invFun p := p.snd.left
+  left_inv _ := by simp
+  right_inv := fun _ => by
+    dsimp; congr! 1 with h
+    . simp
+    . rw! [h]; simp
+
+@[simps]
+def equivalence_Elements (A : 𝒞) : (yoneda.obj A).Elements ≌ (Over A)ᵒᵖ where
+  functor := {
+    obj := fun x => .op <| Over.mk x.snd
+    map := fun f => .op <| Over.homMk f.val.unop (by simpa using f.property)
+  }
+  inverse := {
+    obj := fun U => ⟨.op U.unop.left, U.unop.hom⟩
+    map := fun f => ⟨.op f.unop.left, by simp⟩
+  }
+  unitIso := NatIso.ofComponents Iso.refl (by simp)
+  counitIso := NatIso.ofComponents Iso.refl
+    -- TODO: `simp` fails to unify `id_comp`/`comp_id`
+    (fun f => by simp [Category.comp_id f, Category.id_comp f])
+
+/-- For `X ∈ 𝒞` and `f ∈ 𝒞/A`, `𝒞(X, Over.forget f) ≅ Σ(g: X ⟶ A), 𝒞/A(g, f)`. -/
+def forget_iso_Sigma (A : 𝒞) :
+    Over.forget A ⋙₂ coyoneda (C := 𝒞) ≅
+    Functor.Sigma ((equivalence_Elements A).functor ⋙ coyoneda (C := Over A)) := by
+  refine NatIso.ofComponents₂ (fun X U => Equiv.toIso <| equiv_Sigma X.unop U) ?_ ?_
+  . intros X Y U f
+    ext : 1
+    dsimp
+    apply have h := ?_; Sigma.ext h ?_
+    . simp
+    . dsimp at h ⊢
+      rw! [h]
+      simp
+  . intros X Y U f
+    ext : 1
+    dsimp
+    apply have h := ?_; Sigma.ext h ?_
+    . simp
+    . dsimp at h ⊢
+      rw! [h]
+      apply heq_of_eq
+      ext : 1
+      simp
+
+end CategoryTheory.Over
+
+#min_imports
diff --git a/Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean b/Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean
index f2b046c..4a8ab7b 100644
--- a/Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean
+++ b/Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Sina Hazratpour. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sina Hazratpour
+Authors: Sina Hazratpour, Wojciech Nawrocki
 -/
 import Mathlib.CategoryTheory.Comma.Over.Basic
 import Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
@@ -9,16 +9,36 @@ import Mathlib.CategoryTheory.Category.Cat
 
 namespace CategoryTheory
 
+-- morphism levels before object levels. See note [CategoryTheory universes].
 universe v₁ v₂ v₃ u₁ u₂ u₃
 
--- morphism levels before object levels. See note [CategoryTheory universes].
 variable {T : Type u₁} [Category.{v₁} T]
 
 namespace Over
 
-/-- `Over.Sigma Y U` a shorthand for `(Over.map Y.hom).obj U`. This is the categoy-theoretic
-analogue of `Sigma` for types.
--/
+@[simp]
+theorem mk_eta {X : T} (U : Over X) : mk U.hom = U := by
+  rfl
+
+/-- A variant of `homMk_comp` that can trigger in `simp`. -/
+@[simp]
+lemma homMk_comp' {X Y Z W : T} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (fgh_comp) :
+    homMk (U := mk (f ≫ g ≫ h)) (f ≫ g) fgh_comp =
+    homMk f ≫ homMk (U := mk (g ≫ h)) (V := mk h) g :=
+  rfl
+
+@[simp]
+lemma homMk_comp'_assoc {X Y Z W : T} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (fgh_comp) :
+    homMk (U := mk ((f ≫ g) ≫ h)) (f ≫ g) fgh_comp =
+    homMk f ≫ homMk (U := mk (g ≫ h)) (V := mk h) g := by
+  rfl
+
+@[simp]
+lemma homMk_id {X B : T} (f : X ⟶ B) (h : 𝟙 X ≫ f = f) : homMk (𝟙 X) h = 𝟙 (mk f) :=
+  rfl
+
+/-- `Over.Sigma Y U` is a shorthand for `(Over.map Y.hom).obj U`.
+This is a category-theoretic analogue of `Sigma` for types. -/
 abbrev Sigma {X : T} (Y : Over X) (U : Over (Y.left)) : Over X :=
   (map Y.hom).obj U
 
@@ -32,6 +52,7 @@ lemma hom {Y : Over X} (Z : Over (Y.left)) : (Sigma Y Z).hom = Z.hom ≫ Y.hom :
 def map {Y : Over X} {Z Z' : Over (Y.left)} (g : Z ⟶ Z') : (Sigma Y Z) ⟶ (Sigma Y Z') :=
   (Over.map Y.hom).map g
 
+@[simp]
 lemma map_left {Y : Over X} {Z Z' : Over (Y.left)} {g : Z ⟶ Z'} :
     ((Over.map Y.hom).map g).left = g.left := Over.map_map_left
 
@@ -43,6 +64,7 @@ lemma map_homMk_left {Y : Over X} {Z Z' : Over (Y.left)} {g : Z ⟶ Z'} :
 @[simps!]
 def fst {Y : Over X} (Z : Over (Y.left)) : (Sigma Y Z) ⟶ Y := Over.homMk Z.hom
 
+@[simp]
 lemma map_comp_fst {Y : Over X} {Z Z' : Over (Y.left)} (g : Z ⟶ Z') :
     (Over.map Y.hom).map g ≫ fst Z' = fst Z := by
   ext
diff --git a/Poly/ForMathlib/CategoryTheory/Elements.lean b/Poly/ForMathlib/CategoryTheory/Elements.lean
new file mode 100644
index 0000000..ab84dd6
--- /dev/null
+++ b/Poly/ForMathlib/CategoryTheory/Elements.lean
@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2025 Wojciech Nawrocki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Nawrocki
+-/
+import Mathlib.CategoryTheory.Elements
+
+namespace CategoryTheory.CategoryOfElements
+
+variable {𝒞 𝒟 : Type*} [Category 𝒞] [Category 𝒟]
+variable (F : 𝒞 ⥤ Type*) (G : F.Elements ⥤ 𝒟)
+
+-- FIXME(mathlib): `NatTrans.mapElements` and `CategoryOfElements.map` are the same thing
+
+@[simp]
+theorem map_homMk_id {X : 𝒞} (a : F.obj X) (eq : F.map (𝟙 X) a = a) :
+    -- NOTE: without `α := X ⟶ X`, a bad discrimination tree key involving `⟨X, a⟩.1` is generated.
+    G.map (Subtype.mk (α := X ⟶ X) (𝟙 X) eq) = 𝟙 (G.obj ⟨X, a⟩) :=
+  show G.map (𝟙 _) = 𝟙 _ by simp
+
+@[simp]
+theorem map_homMk_comp {X Y Z : 𝒞} (f : X ⟶ Y) (g : Y ⟶ Z) (a : F.obj X) eq :
+    G.map (Y := ⟨Z, F.map g (F.map f a)⟩) (Subtype.mk (α := X ⟶ Z) (f ≫ g) eq) =
+    G.map (X := ⟨X, a⟩) (Y := ⟨Y, F.map f a⟩) (Subtype.mk (α := X ⟶ Y) f rfl) ≫
+    G.map (Subtype.mk (α := Y ⟶ Z) g (by rfl)) := by
+  set X : F.Elements := ⟨X, a⟩
+  set Y : F.Elements := ⟨Y, F.map f a⟩
+  set Z : F.Elements := ⟨Z, F.map g (F.map f a)⟩
+  set f : X ⟶ Y := ⟨f, rfl⟩
+  set g : Y ⟶ Z := ⟨g, rfl⟩
+  show G.map (f ≫ g) = G.map f ≫ G.map g
+  simp
+
+end CategoryTheory.CategoryOfElements
diff --git a/Poly/ForMathlib/CategoryTheory/NatIso.lean b/Poly/ForMathlib/CategoryTheory/NatIso.lean
new file mode 100644
index 0000000..27b100f
--- /dev/null
+++ b/Poly/ForMathlib/CategoryTheory/NatIso.lean
@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2025 Wojciech Nawrocki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Nawrocki
+-/
+
+import Mathlib.CategoryTheory.NatIso
+
+namespace CategoryTheory.NatIso
+
+variable {𝒞 𝒟 ℰ : Type*} [Category 𝒞] [Category 𝒟] [Category ℰ]
+
+/-- Natural isomorphism of bifunctors from naturality in both arguments. -/
+def ofComponents₂ {F G : 𝒞 ⥤ 𝒟 ⥤ ℰ}
+    (app : ∀ Γ X, (F.obj Γ).obj X ≅ (G.obj Γ).obj X)
+    (naturality₂_left : ∀ {Γ Δ : 𝒞} (X : 𝒟) (σ : Γ ⟶ Δ),
+      (F.map σ).app X ≫ (app Δ X).hom = (app Γ X).hom ≫ (G.map σ).app X := by aesop_cat)
+    (naturality₂_right : ∀ {X Y : 𝒟} (Γ : 𝒞) (f : X ⟶ Y),
+      (F.obj Γ).map f ≫ (app Γ Y).hom = (app Γ X).hom ≫ (G.obj Γ).map f := by aesop_cat) :
+    F ≅ G :=
+  NatIso.ofComponents
+    (fun Γ => NatIso.ofComponents (app Γ) (fun f => by simpa using naturality₂_right Γ f))
+    (fun σ => by ext X : 2; simpa using naturality₂_left X σ)
+
+end CategoryTheory.NatIso
diff --git a/Poly/ForMathlib/CategoryTheory/Types.lean b/Poly/ForMathlib/CategoryTheory/Types.lean
new file mode 100644
index 0000000..b221290
--- /dev/null
+++ b/Poly/ForMathlib/CategoryTheory/Types.lean
@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2025 Wojciech Nawrocki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Nawrocki
+-/
+
+import Mathlib.CategoryTheory.Types
+
+namespace CategoryTheory.FunctorToTypes
+
+/-! Repetitive lemmas about bifunctors into `Type`.
+
+Q: Is there a better way?
+Mathlib doesn't seem to think so:
+see `hom_inv_id_app`, `hom_inv_id_app_app`, `hom_inv_id_app_app_app`.
+Can a `simproc` that tries `congr_fun/congr_arg simpLemma` work? -/
+
+universe w
+variable {𝒞 𝒟 : Type*} [Category 𝒞] [Category 𝒟] (F G : 𝒞 ⥤ 𝒟 ⥤ Type w)
+  {C₁ C₂ : 𝒞} {D₁ D₂ : 𝒟}
+
+theorem naturality₂_left (σ : F ⟶ G) (f : C₁ ⟶ C₂) (x : (F.obj C₁).obj D₁) :
+    (σ.app C₂).app D₁ ((F.map f).app D₁ x) = (G.map f).app D₁ ((σ.app C₁).app D₁ x) :=
+  congr_fun (congr_fun (congr_arg NatTrans.app (σ.naturality f)) D₁) x
+
+theorem naturality₂_right (σ : F ⟶ G) (f : D₁ ⟶ D₂) (x : (F.obj C₁).obj D₁) :
+    (σ.app C₁).app D₂ ((F.obj C₁).map f x) = (G.obj C₁).map f ((σ.app C₁).app D₁ x) :=
+  naturality ..
+
+@[simp]
+theorem hom_inv_id_app_app_apply (α : F ≅ G) (C D) (x) :
+    (α.inv.app C).app D ((α.hom.app C).app D x) = x :=
+  congr_fun (α.hom_inv_id_app_app C D) x
+
+@[simp]
+theorem inv_hom_id_app_app_apply (α : F ≅ G) (C D) (x) :
+    (α.hom.app C).app D ((α.inv.app C).app D x) = x :=
+  congr_fun (α.inv_hom_id_app_app C D) x
diff --git a/Poly/UvPoly.lean b/Poly/UvPoly/Basic.lean
similarity index 79%
rename from Poly/UvPoly.lean
rename to Poly/UvPoly/Basic.lean
index 1f75268..77abc99 100644
--- a/Poly/UvPoly.lean
+++ b/Poly/UvPoly/Basic.lean
@@ -1,13 +1,14 @@
 /-
 Copyright (c) 2024 Sina Hazratpour. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sina Hazratpour
+Authors: Sina Hazratpour, Wojciech Nawrocki
 -/
 
 import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.BeckChevalley -- LCCC.BeckChevalley
 import Mathlib.CategoryTheory.Functor.TwoSquare
 import Poly.ForMathlib.CategoryTheory.PartialProduct
 
+
 /-!
 # Polynomial Functor
 
@@ -72,7 +73,7 @@ def prod {E' B'} (P : UvPoly E B) (Q : UvPoly E' B') [HasBinaryCoproducts C]:
 /-- For a category `C` with binary products, `P.functor : C ⥤ C` is the functor associated
 to a single variable polynomial `P : UvPoly E B`. -/
 def functor [HasBinaryProducts C] (P : UvPoly E B) : C ⥤ C :=
-  Over.star E ⋙ pushforward P.p ⋙ forget B
+  star E ⋙ pushforward P.p ⋙ forget B
 
 /-- The evaluation function of a polynomial `P` at an object `X`. -/
 def apply (P : UvPoly E B) : C → C := (P.functor).obj
@@ -96,11 +97,10 @@ def idApplyIso (X : C) : (id B) @ X ≅ B ⨯ X := sorry
 variable {B}
 
 /-- The fstProjection morphism from `∑ b : B, X ^ (E b)` to `B` again. -/
-@[simp]
 def fstProj (P : UvPoly E B) (X : C) : P @ X ⟶ B :=
   ((Over.star E ⋙ pushforward P.p).obj X).hom
 
-@[simp, reassoc (attr := simp)]
+@[reassoc (attr := simp)]
 lemma map_fstProj {X Y : C} (P : UvPoly E B) (f : X ⟶ Y) :
     P.functor.map f ≫ P.fstProj Y = P.fstProj X := by
   simp [fstProj, functor]
@@ -236,7 +236,7 @@ def Total.ofHom {E' B' : C} (P : UvPoly E B) (Q : UvPoly E' B') (α : P.Hom Q) :
 
 namespace UvPoly
 
-variable {C : Type*} [Category C] [HasTerminal C] [HasPullbacks C]
+variable {C : Type u} [Category.{v} C] [HasTerminal C] [HasPullbacks C]
 
 instance : SMul C (Total C) where
   smul S P := Total.of (smul S P.poly)
@@ -274,7 +274,7 @@ polynomial functor.
 -/
 def isLimitFan (P : UvPoly E B) (X : C) : IsLimit (fan P X) where
   lift c := (pushforwardCurry <| overPullbackToStar c.fst c.snd).left
-  fac_left := by aesop_cat
+  fac_left := by aesop_cat (add norm fstProj)
   fac_right := by
     intro c
     simp only [fan_snd, pullbackMap, ε, ev, ← assoc, ← comp_left]
@@ -302,6 +302,7 @@ abbrev lift {Γ X : C} (P : UvPoly E B) (b : Γ ⟶ B) (e : pullback b P.p ⟶ X
     Γ ⟶ P @ X :=
   partialProd.lift ⟨fan P X, isLimitFan P X⟩ b e
 
+@[simp]
 theorem lift_fst {Γ X : C} {P : UvPoly E B} {b : Γ ⟶ B} {e : pullback b P.p ⟶ X} :
     P.lift b e ≫ P.fstProj X = b := by
   unfold lift
@@ -333,86 +334,13 @@ theorem proj_snd {Γ X : C} {P : UvPoly E B} {f : Γ ⟶ P @ X} :
     (pullback.map _ _ _ _ f (𝟙 E) (𝟙 B) (by aesop) (by aesop)) ≫ ε P X ≫ prod.snd := by
   simp [proj]
 
-/-- Universal property of the polynomial functor. -/
-@[simps]
-def equiv (P : UvPoly E B) (Γ : C) (X : C) :
-    (Γ ⟶ P @ X) ≃ (b : Γ ⟶ B) × (pullback b P.p ⟶ X) where
-  toFun := P.proj
-  invFun u := P.lift (Γ := Γ) (X := X) u.1 u.2
-  left_inv f := by
-    dsimp
-    symm
-    fapply partialProd.hom_ext ⟨fan P X, isLimitFan P X⟩
-    · simp [partialProd.lift]
-      rfl
-    · sorry
-  right_inv := by
-    intro ⟨b, e⟩
-    ext
-    · simp only [proj_fst, lift_fst]
-    · sorry
-
-#exit
-
-/-- `UvPoly.equiv` is natural in `Γ`. -/
-lemma equiv_naturality_left {Δ Γ : C} (σ : Δ ⟶ Γ) (P : UvPoly E B) (X : C)
-    (f : Γ ⟶ P @ X) :
-    equiv P Δ X (σ ≫ f) = let ⟨b, e⟩ := equiv P Γ X f
-                           ⟨σ ≫ b, pullback.lift (pullback.fst .. ≫ σ) (pullback.snd ..)
-                                     (assoc (obj := C) .. ▸ pullback.condition) ≫ e⟩ := by
-  dsimp
-  congr! with h
-  . simp [polyPair, partialProduct.liftAux]
-  . set g := _ ≫ (P.polyPair be).snd
-    rw [(_ : (P.polyPair (σ ≫ be)).snd = (pullback.congrHom h rfl).hom ≫ g)]
-    · generalize (P.polyPair (σ ≫ be)).fst = x at h
-      cases h
-      simp
-    · simp only [polyPair, comp_obj, homEquiv_counit, id_obj, comp_left, pullback_obj_left,
-      mk_left, mk_hom, star_obj_left, pullback_map_left, homMk_left, pullback.congrHom_hom, ←
-      assoc, g]
-      congr 2
-      ext <;> simp
-
-/-- `UvPoly.equiv` is natural in `X`. -/
-lemma equiv_naturality_right {Γ X Y : C}
-    (P : UvPoly E B) (be : Γ ⟶ P.functor.obj X) (f : X ⟶ Y) :
-    equiv P Γ Y (be ≫ P.functor.map f) =
-      let ⟨b, e⟩ := equiv P Γ X be
-      ⟨b, e ≫ f⟩ := by
-  dsimp
-  congr! 1 with h
-  . simp [polyPair]
-  . set g := (P.polyPair be).snd ≫ f
-    rw [(_ : (P.polyPair (be ≫ P.functor.map f)).snd = (pullback.congrHom h rfl).hom ≫ g)]
-    · generalize (P.polyPair (be ≫ P.functor.map f)).fst = x at h
-      cases h
-      simp
-    · dsimp only [polyPair, g]
-      rw [homMk_comp (w_f := by simp [fstProj, functor]) (w_g := by simp [functor])]
-      simp only [UvPoly.functor, Functor.comp_map, forget_map, homMk_eta,
-        homEquiv_naturality_right_symm, comp_left, assoc]
-      admit
-      --rw [show ((Over.pullback E).map f).left ≫ prod.snd = prod.snd ≫ f by simp]
-      -- simp only [← assoc]
-      -- congr 2
-      -- simp only [comp_obj, forget_obj, star_obj_left, homEquiv_counit, id_obj, comp_left,
-      --   pullback_obj_left, mk_left, mk_hom, pullback_map_left, Over.homMk_left,
-      --   pullback.congrHom_hom, ← assoc]
-      -- congr 1
-      -- ext <;> simp
-
 /-- The domain of the composition of two polynomials. See `UvPoly.comp`. -/
 def compDom {E B D A : C} (P : UvPoly E B) (Q : UvPoly D A) :=
   Limits.pullback Q.p (fan P A).snd
 
-/-- The codomain of the composition of two polynomials. See `UvPoly.comp`. -/
-def compCod {E B D A : C} (P : UvPoly E B) (_ : UvPoly D A) :=
-  P @ A
-
 @[simps!]
 def comp [HasPullbacks C] [HasTerminal C]
-    {E B D A : C} (P : UvPoly E B) (Q : UvPoly D A) : UvPoly (compDom P Q) (compCod P Q) :=
+    {E B D A : C} (P : UvPoly E B) (Q : UvPoly D A) : UvPoly (compDom P Q) (P @ A) :=
    {
      p :=  (pullback.snd Q.p (fan P A).snd) ≫ (pullback.fst (fan P A).fst P.p)
      exp := by sorry
@@ -434,12 +362,5 @@ instance monoidal [HasPullbacks C] [HasTerminal C] : MonoidalCategory (UvPoly.To
   rightUnitor := sorry
 
 end UvPoly
-
-
-
-
-
-
 end CategoryTheory
-
 end
diff --git a/Poly/UvPoly/UPFan.lean b/Poly/UvPoly/UPFan.lean
new file mode 100644
index 0000000..7e000fe
--- /dev/null
+++ b/Poly/UvPoly/UPFan.lean
@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2025 Sina Hazratpour. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sina Hazratpour
+-/
+import Poly.UvPoly.Basic
+
+noncomputable section
+
+namespace CategoryTheory.UvPoly
+open Limits PartialProduct
+
+universe v u
+variable {C : Type u} [Category.{v} C] [HasPullbacks C] [HasTerminal C] {E B : C}
+
+/-- Universal property of the polynomial functor. -/
+@[simps]
+def equiv (P : UvPoly E B) (Γ : C) (X : C) :
+    (Γ ⟶ P @ X) ≃ (b : Γ ⟶ B) × (pullback b P.p ⟶ X) where
+  toFun := P.proj
+  invFun u := P.lift (Γ := Γ) (X := X) u.1 u.2
+  left_inv f := by
+    dsimp
+    symm
+    fapply partialProd.hom_ext ⟨fan P X, isLimitFan P X⟩
+    · simp [partialProd.lift]
+      rfl
+    · sorry
+  right_inv := by
+    intro ⟨b, e⟩
+    ext
+    · simp only [proj_fst, lift_fst]
+    · sorry
+
+end CategoryTheory.UvPoly
diff --git a/Poly/UvPoly/UPIso.lean b/Poly/UvPoly/UPIso.lean
new file mode 100644
index 0000000..d6d9eb6
--- /dev/null
+++ b/Poly/UvPoly/UPIso.lean
@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2025 Wojciech Nawrocki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Nawrocki
+-/
+import Poly.UvPoly.Basic
+import Poly.Bifunctor.Sigma
+
+noncomputable section
+
+namespace CategoryTheory.UvPoly
+open Limits Over ExponentiableMorphism Functor
+
+universe v u
+variable {C : Type u} [Category.{v} C] [HasPullbacks C] {E B : C} (P : UvPoly E B)
+
+/-- Sends `(Γ, X)` to `Σ(b : Γ ⟶ B), 𝒞(pullback b P.p, X)`.
+This is equivalent to the type of partial product cones with apex `Γ` over `X`. -/
+@[simps! obj_obj map_app]
+def partProdsOver : Cᵒᵖ ⥤ C ⥤ Type v :=
+  Functor.Sigma
+    ((Over.equivalence_Elements B).functor ⋙ (Over.pullback P.p).op ⋙
+      (forget E).op ⋙ coyoneda (C := C))
+
+@[simp]
+theorem partProdsOver_obj_map {X Y : C} (Γ : Cᵒᵖ) (f : X ⟶ Y) (x : (P.partProdsOver.obj Γ).obj X) :
+    (P.partProdsOver.obj Γ).map f x = ⟨x.1, x.2 ≫ f⟩ := by
+  dsimp [partProdsOver]
+  have : 𝟙 Γ.unop ≫ x.1 = x.1 := by simp
+  ext : 1
+  . simp
+  . dsimp
+    rw! (castMode := .all) [this]
+    simp
+
+variable [HasTerminal C]
+
+/-- `𝒞(Γ, PₚX) ≅ Σ(b : Γ ⟶ B), 𝒞(b*p, X)` -/
+def iso_Sigma (P : UvPoly E B) :
+    P.functor ⋙₂ coyoneda (C := C) ≅ P.partProdsOver :=
+  calc
+    P.functor ⋙₂ coyoneda (C := C) ≅
+        (star E ⋙ pushforward P.p) ⋙₂ (forget B ⋙₂ coyoneda (C := C)) :=
+      Iso.refl _
+
+    _ ≅ (star E ⋙ pushforward P.p) ⋙₂ Functor.Sigma
+        ((equivalence_Elements B).functor ⋙ coyoneda (C := Over B)) :=
+      comp₂_isoWhiskerLeft _ (forget_iso_Sigma B)
+
+    _ ≅ Functor.Sigma
+        ((equivalence_Elements B).functor ⋙
+          star E ⋙₂ pushforward P.p ⋙₂ coyoneda (C := Over B)) :=
+      -- Q: better make `comp₂_Sigma` an iso and avoid `eqToIso`?
+      eqToIso (by simp [comp₂_Sigma])
+
+    _ ≅ _ :=
+      let i :=
+        calc
+          star E ⋙₂ pushforward P.p ⋙₂ coyoneda (C := Over B) ≅
+              star E ⋙₂ (Over.pullback P.p).op ⋙ coyoneda (C := Over E) :=
+            comp₂_isoWhiskerLeft (star E) (Adjunction.coyoneda_iso <| adj P.p).symm
+
+          _ ≅ (Over.pullback P.p).op ⋙ star E ⋙₂ coyoneda (C := Over E) :=
+            Iso.refl _
+
+          _ ≅ (Over.pullback P.p).op ⋙ (forget E).op ⋙ coyoneda (C := C) :=
+            isoWhiskerLeft (Over.pullback P.p).op (Adjunction.coyoneda_iso <| forgetAdjStar E).symm;
+
+      Functor.Sigma.isoCongrRight (isoWhiskerLeft _ i)
+
+def equiv (Γ X : C) : (Γ ⟶ P.functor.obj X) ≃ (b : Γ ⟶ B) × (pullback b P.p ⟶ X) :=
+  Iso.toEquiv <| (P.iso_Sigma.app (.op Γ)).app X
+
+theorem equiv_app (Γ X : C) (be : Γ ⟶ P.functor.obj X) :
+    P.equiv Γ X be = (P.iso_Sigma.hom.app <| .op Γ).app X be := by
+  dsimp [equiv]
+
+-- TODO(WN): Checking the theorem statement takes 5s, and kernel typechecking 10s!
+lemma equiv_naturality_left {Δ Γ : C} (σ : Δ ⟶ Γ) (X : C) (be : Γ ⟶ P.functor.obj X) :
+    P.equiv Δ X (σ ≫ be) =
+      let p := P.equiv Γ X be
+      ⟨σ ≫ p.1, pullback.lift (pullback.fst .. ≫ σ) (pullback.snd ..)
+        (Category.assoc (obj := C) .. ▸ pullback.condition) ≫ p.2⟩ := by
+  conv_lhs => rw [equiv_app, coyoneda.comp₂_naturality₂_left, ← equiv_app]
+  simp
+
+-- TODO(WN): Kernel typechecking takes 10s!
+lemma equiv_naturality_right {Γ X Y : C} (be : Γ ⟶ P.functor.obj X) (f : X ⟶ Y) :
+    equiv P Γ Y (be ≫ P.functor.map f) =
+      let p := equiv P Γ X be
+      ⟨p.1, p.2 ≫ f⟩ := by
+  conv_lhs => rw [equiv_app, coyoneda.comp₂_naturality₂_right, ← equiv_app]
+  simp
+
+end CategoryTheory.UvPoly
diff --git a/Poly/deprecated/Basic.lean b/Poly/deprecated/Basic.lean
index 2494521..bc69ad1 100644
--- a/Poly/deprecated/Basic.lean
+++ b/Poly/deprecated/Basic.lean
@@ -7,7 +7,7 @@ Authors: Emily Riehl, Sina Hazratpour, Wojciech Nawrocki
 import Mathlib.CategoryTheory.Adjunction.Over
 import Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
 import Mathlib.CategoryTheory.ChosenFiniteProducts
-import Poly.ForMathlib
+import Poly.deprecated.ForMathlib
 
 /-!
 # Some basic equalities and isomorphisms of composition and base change functors
diff --git a/Poly/ForMathlib.lean b/Poly/deprecated/ForMathlib.lean
similarity index 100%
rename from Poly/ForMathlib.lean
rename to Poly/deprecated/ForMathlib.lean
diff --git a/lake-manifest.json b/lake-manifest.json
index c855062..746537a 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,7 +1,17 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/mathlib4.git",
+ [{"url": "https://github.com/Vtec234/lean4-seq",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "b6b76a5d7cc1c8b11c52f12a7bd90c460b7cba5a",
+   "name": "seq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
diff --git a/lakefile.lean b/lakefile.lean
index d49f5c4..c6f3ad7 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -11,6 +11,8 @@ package «Poly» where
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git"
 
+require seq from git "https://github.com/Vtec234/lean4-seq"
+
 @[default_target]
 lean_lib «Poly» where
   -- add any library configuration options here