diff --git a/Poly/Bifunctor/Basic.lean b/Poly/Bifunctor/Basic.lean
index 17503a9..c434164 100644
--- a/Poly/Bifunctor/Basic.lean
+++ b/Poly/Bifunctor/Basic.lean
@@ -35,15 +35,16 @@ theorem comp₂_comp {𝒞' : Type*} [Category 𝒞']
     (F : 𝒞' ⥤ 𝒞) (G : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) :
     G ⋙₂ (F ⋙ P) = F ⋙ (G ⋙₂ P) := rfl
 
+set_option backward.defeqAttrib.useBackward true in
 @[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])
+    (fun {Γ Δ} X σ => by cat_disch)
+    (fun {X Y} C f => by
+      dsimp
+      simp only [Category.assoc, NatTrans.naturality_assoc, ← Functor.map_comp,
+        i.hom.naturality])
 
 @[simps!]
 def comp₂_isoWhiskerLeft {P₁ P₂ : 𝒞 ⥤ 𝒟 ⥤ ℰ} (F : 𝒟' ⥤ 𝒟) (i : P₁ ≅ P₂) :
@@ -69,13 +70,13 @@ 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]
+    (i.app <| .op X).app Z (f ≫ g) = (P.map f.op).app Z ((i.app <| .op Y).app Z g) :=
+  FunctorToTypes.naturality₂_left (F ⋙₂ coyoneda (C := 𝒞)) P i f.op g
 
 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]
+    (i.app <| .op X).app Z (f ≫ F.map g) = (P.obj <| .op X).map g ((i.app <| .op X).app Y f) :=
+  FunctorToTypes.naturality₂_right (F ⋙₂ coyoneda (C := 𝒞)) P i g f
 
 end coyoneda
 
@@ -87,8 +88,8 @@ variable {𝒟 : Type*} [Category 𝒟]
 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])
+    (fun _ _ => by ext g; exact A.homEquiv_naturality_left _ _)
+    (fun _ _ => by ext g; exact A.homEquiv_naturality_right _ _)
 
 end Adjunction
 end CategoryTheory
diff --git a/Poly/Bifunctor/Sigma.lean b/Poly/Bifunctor/Sigma.lean
index d453d2d..540f388 100644
--- a/Poly/Bifunctor/Sigma.lean
+++ b/Poly/Bifunctor/Sigma.lean
@@ -45,19 +45,36 @@ a functor `F'` s.t. `F'.Elements ≅ F.Elements × 𝒟`; very awkward.
 - 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)⟩
+    obj := fun CD => (a : F.obj CD.1) × (G.obj ⟨CD.1, a⟩).obj CD.2
+    map := fun fg => TypeCat.ofHom fun ab =>
+      ⟨F.map fg.1 ab.1, (G.map ⟨fg.1, rfl⟩).app _ ((G.obj ⟨_, ab.1⟩).map fg.2 ab.2)⟩
     map_id := ?_
     map_comp := ?_
-  } <;> {
-    intros
-    ext ⟨a, b⟩ : 1
-    dsimp
-    congr! 1 with h
-    . simp
-    . rw! [h]; simp [FunctorToTypes.naturality]
   }
+  · intro X
+    apply ConcreteCategory.ext_apply
+    rintro ⟨a, b⟩
+    simp only [TypeCat.ofHom_apply, types_id_apply]
+    dsimp
+    refine Sigma.ext (by simp) ?_
+    have hobj : F.elementsMk X.1 a = F.elementsMk X.1 (F.map (𝟙 X.1) a) := by
+      simp [Functor.map_id_apply]
+    have key : (⟨𝟙 X.1, rfl⟩ :
+          F.elementsMk X.1 a ⟶ F.elementsMk X.1 (F.map (𝟙 X.1) a))
+        = eqToHom hobj := by
+      apply (CategoryOfElements.π F).map_injective
+      simp [CategoryOfElements.π, eqToHom_map]
+    rw [key]
+    simp [eqToHom_map, eqToHom_app]
+  · intro X Y Z f g
+    apply ConcreteCategory.ext_apply
+    rintro ⟨a, b⟩
+    simp only [TypeCat.ofHom_apply, types_comp_apply]
+    dsimp
+    refine Sigma.ext (by simp) ?_
+    rw! (castMode := .all)
+      [show F.map (f.1 ≫ g.1) a = F.map g.1 (F.map f.1 a) from by simp]
+    simp [NatTrans.naturality_apply]
 
 def Sigma.isoCongrLeft {F₁ F₂ : 𝒞 ⥤ Type w}
     /- Q: What kind of map `F₂.Elements ⥤ F₁.Elements`
diff --git a/Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean b/Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean
index c7d37a7..0abbddf 100644
--- a/Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean
+++ b/Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean
@@ -35,10 +35,6 @@ lemma homMk_comp'_assoc {X Y Z W : T} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W)
 lemma homMk_id {X B : T} (f : X ⟶ B) (h : 𝟙 X ≫ f = f) : homMk (𝟙 X) h = 𝟙 (mk f) :=
   rfl
 
-@[simp]
-theorem mkIdTerminal_from_left {B : T} (U : Over B) : (mkIdTerminal.from U).left = U.hom := by
-  simp [mkIdTerminal, CostructuredArrow.mkIdTerminal, Limits.IsTerminal.from, Functor.preimage]
-
 /-- `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 :=
diff --git a/Poly/ForMathlib/CategoryTheory/NatTrans.lean b/Poly/ForMathlib/CategoryTheory/NatTrans.lean
index 6fd36bb..77c20ac 100644
--- a/Poly/ForMathlib/CategoryTheory/NatTrans.lean
+++ b/Poly/ForMathlib/CategoryTheory/NatTrans.lean
@@ -6,7 +6,9 @@ Authors: Sina Hazratpour
 
 import Mathlib.CategoryTheory.NatTrans
 import Mathlib.CategoryTheory.Functor.TwoSquare
-import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
+import Mathlib.CategoryTheory.Discrete.Basic
+import Mathlib.CategoryTheory.Limits.Shapes.Terminal
+import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
 
 open CategoryTheory Limits IsPullback
 
@@ -69,16 +71,10 @@ theorem hcomp {K : Type*} [Category K] {F G : J ⥤ C} {M N : C ⥤ K} {α : F 
     (hα : IsCartesian α) (hβ : IsCartesian β)
     [∀ (i j : J) (f : j ⟶ i), PreservesLimit (cospan (α.app i) (G.map f)) M] :
     IsCartesian (NatTrans.hcomp α β) := by
-  have ha := hα.whiskerRight M
-  have hb := hβ.whiskerLeft G
-  have hc := ha.comp hb
-  unfold IsCartesian
-  intros i j f
-  specialize hc f
-  simp only [Functor.comp_obj, Functor.comp_map, comp_app,
-    whiskerRight_app, whiskerLeft_app,
-    naturality] at hc
-  exact hc
+  have : NatTrans.hcomp α β = Functor.whiskerRight α M ≫ Functor.whiskerLeft G β := by
+    ext x; exact (β.naturality (α.app x)).symm
+  rw [this]
+  exact (hα.whiskerRight M).comp (hβ.whiskerLeft G)
 
 open TwoSquare
 
diff --git a/Poly/ForMathlib/CategoryTheory/Types.lean b/Poly/ForMathlib/CategoryTheory/Types.lean
index 3eb6659..068fdd0 100644
--- a/Poly/ForMathlib/CategoryTheory/Types.lean
+++ b/Poly/ForMathlib/CategoryTheory/Types.lean
@@ -20,19 +20,22 @@ variable {𝒞 𝒟 : Type*} [Category 𝒞] [Category 𝒟] (F G : 𝒞 ⥤ 
   {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
+    (σ.app C₂).app D₁ ((F.map f).app D₁ x) = (G.map f).app D₁ ((σ.app C₁).app D₁ x) := by
+  simpa only [NatTrans.comp_app, types_comp_apply]
+    using types_congr_hom (NatTrans.congr_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 ..
+  NatTrans.naturality_apply ..
 
 @[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
+    (α.inv.app C).app D ((α.hom.app C).app D x) = x := by
+  simpa only [types_comp_apply, types_id_apply]
+    using types_congr_hom (α.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
+    (α.hom.app C).app D ((α.inv.app C).app D x) = x := by
+  simpa only [types_comp_apply, types_id_apply]
+    using types_congr_hom (α.inv_hom_id_app_app C D) x
diff --git a/Poly/Type/Univariate.lean b/Poly/Type/Univariate.lean
index 988caad..8d17ab1 100644
--- a/Poly/Type/Univariate.lean
+++ b/Poly/Type/Univariate.lean
@@ -149,7 +149,7 @@ def sumEquiv : (P.sum Q) X ≃ P X ⊕ Q X where
     | Sum.inl ⟨b, x⟩ => ⟨Sum.inl b, x⟩
     | Sum.inr ⟨b, x⟩ => ⟨Sum.inr b, x⟩
   left_inv := by
-    sorry
+    rintro ⟨(b | b), x⟩ <;> rfl
   right_inv := by
     aesop_cat
 
@@ -177,7 +177,7 @@ theorem map_map (f : X → Y) (g : Y → Z) :
 /-- The associated functor of `P : Poly`. -/
 def functor : Type u ⥤ Type u where
   obj X := P X
-  map {X Y} f := P.map f
+  map {X Y} f := ↾(P.map f)
 
 variable {P}
 
@@ -189,7 +189,7 @@ def Obj.iget [DecidableEq P.B] {X} [Inhabited X] (x : P X) (i : P.Total) : X :=
 @[simp]
 theorem iget_map [DecidableEq P.B] [Inhabited X] [Inhabited Y] (x : P X)
     (f : X → Y) (i : P.Total) (h : i.1 = x.1) : (P.map f x).iget i = f (x.iget i) := by
-  simp only [Obj.iget, fst_map, *, dif_pos, eq_self_iff_true]
+  simp only [Obj.iget, fst_map, *, dif_pos]
   cases x
   rfl
 
@@ -224,12 +224,12 @@ def comp.mk {X : Type u} (x : P (Q X)) : Q.comp P X :=
 /-- Functor composition for polynomial functors in the diagrammatic order. -/
 def comp.functor : Poly.functor (Q.comp P) ≅ Poly.functor Q ⋙ Poly.functor P where
   hom := {
-    app := fun X => fun ⟨b,e⟩ =>
+    app := fun X => ↾fun ⟨b,e⟩ =>
     ⟨ b.1, fun x' => ⟨ b.2 x', fun b' => e ⟨x',b'⟩ ⟩⟩
     naturality := by aesop_cat
   }
   inv := {
-    app X := comp.mk P Q
+    app X := ↾comp.mk P Q
     naturality := by aesop_cat
   }
 
diff --git a/lake-manifest.json b/lake-manifest.json
index fe87d44..1cd0103 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,4 +1,4 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/PatrickMassot/checkdecls.git",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "dd5e5d97469dec395f29661366030566355ad9be",
+   "rev": "5a6fc726c807c8625f1abfdfe710464adb658e69",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b3dd6c3ebc0a71685e86bea9223be39ea4c299fb",
+   "rev": "9196a81145e1e291a1469288e77392b0e1b9a493",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cff9dd30f2c161b9efd7c657cafed1f967645890",
+   "rev": "6db47de43aa7f516708053ae2fdadd29dd9baaaa",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,51 +55,52 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ef8377f31b5535430b6753a974d685b0019d0681",
+   "rev": "85bb7e7637e84a7d9803be7d954579fdae42c64b",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.84",
+   "inputRev": "v0.0.100",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fa78cf032194308a950a264ed87b422a2a7c1c6c",
+   "rev": "fafca80479ff95e041d84373dda7122adf1295f2",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.31.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8920dcbb96a4e8bf641fc399ac9c0888e4a6be72",
+   "rev": "8d33324ee877e9735d2829bc6f1f439e60cf98b1",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.31.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dff865b7ee7011518d59abfc101c368293173150",
+   "rev": "708b057842c4cd0845fba132bd94b08493f6fc42",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.31.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60",
+   "rev": "48bdcff4c5fa27e09028f9f330e59baa0d4640cf",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0-rc1",
+   "inputRev": "v4.31.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "Poly",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/lean-toolchain b/lean-toolchain
index fb18a7f..7217ff5 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.27.0-rc1
\ No newline at end of file
+leanprover/lean4:v4.31.0-rc1
\ No newline at end of file