From 5089fc0b783d143de26ec8723b7d4a06e700ee8c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sat, 30 Dec 2023 20:00:40 +0100
Subject: [PATCH 01/16] Adapt to Coq PR #18845 fixing an issue with maximal
 implicit arguments for notations.

The new (originally intended) behaviour for selecting maximal implicit
arguments of a notation for an applied constant in the presence of
multiple signatures of implicit arguments. Such notations now behave
like ordinary constants or abbreviations for non applied constants,
that is, they complete the application with as much implicit arguments
as possible.

This impacts the notation "naturality[ x ] := (@naturality _ _ _ _ x)"
which is now resolved with 3 trailing implicit arguments, making
tactics such as a "srewrite (naturality[foo])" failing with unresolved
arguments.

It happens that the "naturality" constant mostly uses one signature of
implicit arguments. So, the adaptation is to restrict "naturality" to
only this signature.
---
 Theory/Natural/Transformation.v | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/Theory/Natural/Transformation.v b/Theory/Natural/Transformation.v
index a0edb7ff..c23d9d78 100644
--- a/Theory/Natural/Transformation.v
+++ b/Theory/Natural/Transformation.v
@@ -46,10 +46,8 @@ Qed.
 End Transform.
 
 Arguments transform {_ _ _ _} _ _.
-Arguments naturality
-  {_ _ _ _ _ _ _ _}, {_ _ _ _} _ {_ _ _}, {_ _ _ _} _ _ _ _.
-Arguments naturality_sym
-  {_ _ _ _ _ _ _ _}, {_ _ _ _} _ {_ _ _}, {_ _ _ _} _ _ _ _.
+Arguments naturality {_ _ _ _} _ _ _ _.
+Arguments naturality_sym {_ _ _ _} _ _ _ _.
 
 Declare Scope transform_scope.
 Declare Scope transform_type_scope.
@@ -214,8 +212,8 @@ Program Definition whisker_right {C D : Category} {F G : C ⟶ D} `(N : F ⟹ G)
         {E : Category} (X : E ⟶ C) : F ◯ X ⟹ G ◯ X := {|
   transform := λ x, N (X x);
 
-  naturality     := λ _ _ _, naturality;
-  naturality_sym := λ _ _ _, naturality_sym
+  naturality     := λ _ _ _, naturality _ _ _ _;
+  naturality_sym := λ _ _ _, naturality_sym _ _ _ _
 |}.
 
 Notation "N ⊲ F" := (whisker_right N F) (at level 10).

From 303c221bf35c8af395bcd6d985d23cbc63f36cd3 Mon Sep 17 00:00:00 2001
From: John Wiegley <johnw@newartisans.com>
Date: Tue, 30 Jan 2024 11:25:40 -0800
Subject: [PATCH 02/16] Use 8.19

---
 .github/workflows/coq-ci.yml |  1 +
 default.nix                  | 19 +++++++++++++------
 2 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/coq-ci.yml b/.github/workflows/coq-ci.yml
index 6363f600..76a3fe1b 100644
--- a/.github/workflows/coq-ci.yml
+++ b/.github/workflows/coq-ci.yml
@@ -9,6 +9,7 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.19'
           - 'coqorg/coq:8.18'
           - 'coqorg/coq:8.17'
           - 'coqorg/coq:8.16'
diff --git a/default.nix b/default.nix
index 76fcc5d6..50a332bb 100644
--- a/default.nix
+++ b/default.nix
@@ -1,6 +1,6 @@
 args@{
-  rev    ? "8b5ab8341e33322e5b66fb46ce23d724050f6606"
-, sha256 ? "05ynih3wc7shg324p7icz21qx71ckivzdhkgf5xcvdz6a407v53h"
+  rev    ? "90f456026d284c22b3e3497be980b2e47d0b28ac"
+, sha256 ? "164lsq7xjjvpga6l6lfi9wfsnshgfxnpa8lvb2imscdwgmajakrc"
 
 , pkgs   ? import (builtins.fetchTarball {
     url = "https://github.com/NixOS/nixpkgs/archive/${rev}.tar.gz";
@@ -45,6 +45,11 @@ equations = coqPackages:
      then {
        rev = "v1.3-8.18";
        sha256 = "sha256-8MZO9vWdr8wlAov0lBTYMnde0RuMyhaiM99zp7Zwfao=";
+     } else {}) //
+    (if coqPackages == "coqPackages_8_19"
+     then {
+       rev = "v1.3-8.19";
+       sha256 = "sha256-roBCWfAHDww2Z2JbV5yMI3+EOfIsv3WvxEcUbBiZBsk=";
      } else {}));
 
     phases = [
@@ -70,7 +75,7 @@ equations = coqPackages:
     env = pkgs.buildEnv { inherit name; paths = buildInputs; };
     passthru = {
       compatibleCoqVersions = v:
-        builtins.elem v [ "8.14" "8.15" "8.16" "8.17" "8.18" ];
+        builtins.elem v [ "8.14" "8.15" "8.16" "8.17" "8.18" "8.19" ];
     };
   };
 
@@ -87,7 +92,8 @@ category-theory = coqPackages:
       coq coq.ocaml coq.findlib (equations coqPackages)
     ] ++ pkgs.lib.optionals (coqPackages != "coqPackages_8_16" &&
                              coqPackages != "coqPackages_8_17" &&
-                             coqPackages != "coqPackages_8_18") [
+                             coqPackages != "coqPackages_8_18" &&
+                             coqPackages != "coqPackages_8_19") [
       dpdgraph
     ];
     enableParallelBuilding = true;
@@ -105,7 +111,7 @@ category-theory = coqPackages:
     env = pkgs.buildEnv { inherit name; paths = buildInputs; };
     passthru = {
       compatibleCoqVersions = v:
-        builtins.elem v [ "8.14" "8.15" "8.16" "8.17" "8.18" ];
+        builtins.elem v [ "8.14" "8.15" "8.16" "8.17" "8.18" "8.19" ];
     };
   };
 
@@ -116,5 +122,6 @@ in rec {
   category-theory_8_16 = category-theory "coqPackages_8_16";
   category-theory_8_17 = category-theory "coqPackages_8_17";
   category-theory_8_18 = category-theory "coqPackages_8_18";
-  category-theory_cur  = category-theory_8_18;
+  category-theory_8_19 = category-theory "coqPackages_8_19";
+  category-theory_cur  = category-theory_8_19;
 }

From 17bdf54b56dd50e87daf76fdabf8932795109f10 Mon Sep 17 00:00:00 2001
From: John Wiegley <johnw@newartisans.com>
Date: Tue, 30 Jan 2024 11:33:01 -0800
Subject: [PATCH 03/16] Update check script

---
 check | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/check b/check
index e4bc270c..ff5d5b5f 100755
--- a/check
+++ b/check
@@ -5,8 +5,11 @@ git clean -dfx
 nix-build --cores 4 . --argstr coqPackages coqPackages_8_14 > log_8_14.txt 2>&1 &
 nix-build --cores 4 . --argstr coqPackages coqPackages_8_15 > log_8_15.txt 2>&1 &
 nix-build --cores 4 . --argstr coqPackages coqPackages_8_16 > log_8_16.txt 2>&1 &
+nix-build --cores 4 . --argstr coqPackages coqPackages_8_17 > log_8_17.txt 2>&1 &
+nix-build --cores 4 . --argstr coqPackages coqPackages_8_18 > log_8_18.txt 2>&1 &
+nix-build --cores 4 . --argstr coqPackages coqPackages_8_19 > log_8_19.txt 2>&1 &
 
-docker run -t coqorg/coq:8.16 bash -c '
+docker run -t coqorg/coq:8.19 bash -c '
     git clone https://github.com/jwiegley/category-theory;
     cd category-theory;
     opam update;

From 26eb68886addf6fe09795a1d8df0093194373528 Mon Sep 17 00:00:00 2001
From: John Wiegley <johnw@newartisans.com>
Date: Tue, 30 Jan 2024 11:46:52 -0800
Subject: [PATCH 04/16] Update OPAM file for 8.19

---
 coq-category-theory.opam | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/coq-category-theory.opam b/coq-category-theory.opam
index f70ff04b..6434606b 100644
--- a/coq-category-theory.opam
+++ b/coq-category-theory.opam
@@ -15,7 +15,7 @@ practical work.
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.14" & < "8.19~") | (= "dev")}
+  "coq" {(>= "8.14" & < "8.20~") | (= "dev")}
   "coq-equations" {(>= "1.2" & < "1.4~") | (= "dev")}
 ]
 

From e2d060b252270a0c4a4679236ca98d0d852df18c Mon Sep 17 00:00:00 2001
From: John Wiegley <johnw@newartisans.com>
Date: Tue, 30 Jan 2024 12:02:31 -0800
Subject: [PATCH 05/16] Make a use of counit more explicit

---
 Monad/Adjunction.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Monad/Adjunction.v b/Monad/Adjunction.v
index f4613cfd..d8b4703a 100644
--- a/Monad/Adjunction.v
+++ b/Monad/Adjunction.v
@@ -75,7 +75,7 @@ Proof.
   - simpl.
     srewrite (@fmap_counit_unit); cat.
   - rewrite <- !fmap_comp.
-    srewrite (naturality[counit]); cat.
+    now srewrite (naturality[counit[X]]).
 Qed.
 
 End AdjunctionMonad.

From 4501fb380b83a24c519227096a3db8110a67acc6 Mon Sep 17 00:00:00 2001
From: John Wiegley <johnw@newartisans.com>
Date: Tue, 30 Jan 2024 12:56:12 -0800
Subject: [PATCH 06/16] Another fix to the check script

---
 check | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/check b/check
index ff5d5b5f..ae397fb8 100755
--- a/check
+++ b/check
@@ -9,7 +9,7 @@ nix-build --cores 4 . --argstr coqPackages coqPackages_8_17 > log_8_17.txt 2>&1
 nix-build --cores 4 . --argstr coqPackages coqPackages_8_18 > log_8_18.txt 2>&1 &
 nix-build --cores 4 . --argstr coqPackages coqPackages_8_19 > log_8_19.txt 2>&1 &
 
-docker run -t coqorg/coq:8.19 bash -c '
+docker run -t coqorg/coq:dev bash -c '
     git clone https://github.com/jwiegley/category-theory;
     cd category-theory;
     opam update;

From a67a044ff425660865267b9ae7d5208588c6c6cf Mon Sep 17 00:00:00 2001
From: John Wiegley <johnw@newartisans.com>
Date: Tue, 30 Jan 2024 13:37:02 -0800
Subject: [PATCH 07/16] Another attempt at fixing the counit problem for
 coq:dev

---
 Monad/Adjunction.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/Monad/Adjunction.v b/Monad/Adjunction.v
index d8b4703a..9d854a46 100644
--- a/Monad/Adjunction.v
+++ b/Monad/Adjunction.v
@@ -75,7 +75,9 @@ Proof.
   - simpl.
     srewrite (@fmap_counit_unit); cat.
   - rewrite <- !fmap_comp.
-    now srewrite (naturality[counit[X]]).
+    apply fmap_respects.
+    symmetry.
+    apply (naturality[counit]).
 Qed.
 
 End AdjunctionMonad.

From 48ea563e8496459bd0ccd6eda7f7dd00de2d6587 Mon Sep 17 00:00:00 2001
From: John Wiegley <johnw@newartisans.com>
Date: Tue, 30 Jan 2024 13:48:57 -0800
Subject: [PATCH 08/16] More fixes

---
 Adjunction/Natural/Transformation/Universal.v | 24 ++++++++-----------
 1 file changed, 10 insertions(+), 14 deletions(-)

diff --git a/Adjunction/Natural/Transformation/Universal.v b/Adjunction/Natural/Transformation/Universal.v
index e96faed2..998c41ee 100644
--- a/Adjunction/Natural/Transformation/Universal.v
+++ b/Adjunction/Natural/Transformation/Universal.v
@@ -23,45 +23,41 @@ Program Definition Adjunction_from_Transform (A : F ∹ U) : F ⊣ U := {|
      ; from := {| morphism := fun f =>
          @Transformation.counit _ _ _ _ A b ∘ fmap f |} |}
 |}.
-Next Obligation. proper; rewrites; reflexivity. Qed.
-Next Obligation. proper; rewrites; reflexivity. Qed.
+Next Obligation. proper; now rewrites. Qed.
+Next Obligation. proper; now rewrites. Qed.
 Next Obligation.
   rewrite fmap_comp.
   rewrite <- comp_assoc.
-  srewrite (naturality[Transformation.unit]).
+  srewrite (naturality[unit[A]]).
   rewrite comp_assoc.
   srewrite (@Transformation.fmap_counit_unit); cat.
 Qed.
 Next Obligation.
   rewrite fmap_comp.
   rewrite comp_assoc.
-  srewrite_r (naturality[Transformation.counit]).
+  srewrite_r (naturality[counit[A]]).
   rewrite <- comp_assoc.
   srewrite (@Transformation.counit_fmap_unit); cat.
 Qed.
 Next Obligation.
   rewrite fmap_comp.
   rewrite <- comp_assoc.
-  srewrite (naturality[Transformation.unit]).
-  rewrite comp_assoc.
-  reflexivity.
+  srewrite (naturality[unit[A]]).
+  now rewrite comp_assoc.
 Qed.
 Next Obligation.
   rewrite fmap_comp.
-  rewrite comp_assoc.
-  reflexivity.
+  now rewrite comp_assoc.
 Qed.
 Next Obligation.
   rewrite fmap_comp.
-  rewrite comp_assoc.
-  reflexivity.
+  now rewrite comp_assoc.
 Qed.
 Next Obligation.
   rewrite fmap_comp.
   rewrite comp_assoc.
-  srewrite_r (naturality[Transformation.counit]).
-  rewrite <- comp_assoc.
-  reflexivity.
+  srewrite_r (naturality[counit[A]]).
+  now rewrite <- comp_assoc.
 Qed.
 
 Program Definition Adjunction_to_Transform {A : F ⊣ U} : F ∹ U := {|

From 9a17d8b639ccf5968148d8d798a2986d8e21e3bb Mon Sep 17 00:00:00 2001
From: John Wiegley <johnw@newartisans.com>
Date: Tue, 30 Jan 2024 14:08:11 -0800
Subject: [PATCH 09/16] Another attempt at being more specific

---
 Adjunction/Natural/Transformation/Universal.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Adjunction/Natural/Transformation/Universal.v b/Adjunction/Natural/Transformation/Universal.v
index 998c41ee..dedf46c2 100644
--- a/Adjunction/Natural/Transformation/Universal.v
+++ b/Adjunction/Natural/Transformation/Universal.v
@@ -28,21 +28,21 @@ Next Obligation. proper; now rewrites. Qed.
 Next Obligation.
   rewrite fmap_comp.
   rewrite <- comp_assoc.
-  srewrite (naturality[unit[A]]).
+  srewrite (naturality[@Transformation.unit _ _ _ _ A]).
   rewrite comp_assoc.
   srewrite (@Transformation.fmap_counit_unit); cat.
 Qed.
 Next Obligation.
   rewrite fmap_comp.
   rewrite comp_assoc.
-  srewrite_r (naturality[counit[A]]).
+  srewrite_r (naturality[@Transformation.counit _ _ _ _ A]).
   rewrite <- comp_assoc.
   srewrite (@Transformation.counit_fmap_unit); cat.
 Qed.
 Next Obligation.
   rewrite fmap_comp.
   rewrite <- comp_assoc.
-  srewrite (naturality[unit[A]]).
+  srewrite (naturality[@Transformation.unit _ _ _ _ A]).
   now rewrite comp_assoc.
 Qed.
 Next Obligation.
@@ -56,7 +56,7 @@ Qed.
 Next Obligation.
   rewrite fmap_comp.
   rewrite comp_assoc.
-  srewrite_r (naturality[counit[A]]).
+  srewrite_r (naturality[@Transformation.counit _ _ _ _ A]).
   now rewrite <- comp_assoc.
 Qed.
 

From 5336ee1697c956dfe7db4234fb8ecc8eb3642ebb Mon Sep 17 00:00:00 2001
From: John Wiegley <johnw@newartisans.com>
Date: Tue, 30 Jan 2024 15:50:56 -0800
Subject: [PATCH 10/16] Simplify two definitions

---
 Theory/Kan/Extension.v | 18 ++----------------
 1 file changed, 2 insertions(+), 16 deletions(-)

diff --git a/Theory/Kan/Extension.v b/Theory/Kan/Extension.v
index 3a20455c..c2a8f3d6 100644
--- a/Theory/Kan/Extension.v
+++ b/Theory/Kan/Extension.v
@@ -54,15 +54,8 @@ Class LocalRightKan (X : A ⟶ C) := {
 #[export] Program Instance RightKan_to_LocalRightKan {R : RightKan} (X : A ⟶ C) :
   LocalRightKan X := {|
   LocalRan := Ran X;
-  ran_transform :=
-    let adj_from := from (@adj _ _ _ _ ran_adjoint (Ran X) X) nat_id in
-    {| transform  := transform[adj_from]
-     ; naturality := naturality[adj_from] |}
+  ran_transform := from (@adj _ _ _ _ ran_adjoint (Ran X) X) nat_id
 |}.
-Next Obligation.
-  srewrite_r (naturality[from (@adj _ _ _ _ ran_adjoint (Ran X) X) nat_id]).
-  reflexivity.
-Qed.
 Next Obligation.
   exists (to (@adj _ _ _ _ (@ran_adjoint R) M X) μ).
   - intros.
@@ -112,15 +105,8 @@ Class LocalLeftKan (X : A ⟶ C) := {
 #[export] Program Instance LeftKan_to_LocalLeftKan {R : LeftKan} (X : A ⟶ C) :
   LocalLeftKan X := {|
   LocalLan := Lan X;
-  lan_transform :=
-    let adj_to := to (@adj _ _ _ _ lan_adjoint X (Lan X)) nat_id in
-    {| transform  := transform[adj_to]
-     ; naturality := naturality[adj_to] |}
+  lan_transform := to (@adj _ _ _ _ lan_adjoint X (Lan X)) nat_id
 |}.
-Next Obligation.
-  srewrite_r (naturality[to (@adj _ _ _ _ lan_adjoint X (Lan X)) nat_id]).
-  reflexivity.
-Qed.
 Next Obligation.
   exists (from (@adj _ _ _ _ (@lan_adjoint R) X M) ε).
   - intros.

From 3908290962fcd2148966e3194de3b0c41e76f93d Mon Sep 17 00:00:00 2001
From: John Wiegley <johnw@newartisans.com>
Date: Tue, 30 Jan 2024 16:10:18 -0800
Subject: [PATCH 11/16] Minor work in
 Adjunction/Natural/Transformation/Universal.v

---
 Adjunction/Natural/Transformation/Universal.v | 18 ++++++++----------
 1 file changed, 8 insertions(+), 10 deletions(-)

diff --git a/Adjunction/Natural/Transformation/Universal.v b/Adjunction/Natural/Transformation/Universal.v
index dedf46c2..6a1f7d4b 100644
--- a/Adjunction/Natural/Transformation/Universal.v
+++ b/Adjunction/Natural/Transformation/Universal.v
@@ -18,31 +18,29 @@ Context {U : C ⟶ D}.
 
 Program Definition Adjunction_from_Transform (A : F ∹ U) : F ⊣ U := {|
   adj := fun a b =>
-    {| to   := {| morphism := fun f =>
-         fmap f ∘ @Transformation.unit _ _ _ _ A a |}
-     ; from := {| morphism := fun f =>
-         @Transformation.counit _ _ _ _ A b ∘ fmap f |} |}
+    {| to   := {| morphism := fun f =>n fmap f ∘ transform[unit[A]] a |}
+     ; from := {| morphism := fun f => transform[counit[A]] b ∘ fmap f |} |}
 |}.
 Next Obligation. proper; now rewrites. Qed.
 Next Obligation. proper; now rewrites. Qed.
 Next Obligation.
   rewrite fmap_comp.
   rewrite <- comp_assoc.
-  srewrite (naturality[@Transformation.unit _ _ _ _ A]).
+  srewrite (naturality[unit[A]]).
   rewrite comp_assoc.
   srewrite (@Transformation.fmap_counit_unit); cat.
 Qed.
 Next Obligation.
   rewrite fmap_comp.
   rewrite comp_assoc.
-  srewrite_r (naturality[@Transformation.counit _ _ _ _ A]).
+  srewrite_r (naturality[counit[A]]).
   rewrite <- comp_assoc.
   srewrite (@Transformation.counit_fmap_unit); cat.
 Qed.
 Next Obligation.
   rewrite fmap_comp.
   rewrite <- comp_assoc.
-  srewrite (naturality[@Transformation.unit _ _ _ _ A]).
+  srewrite (naturality[unit[A]]).
   now rewrite comp_assoc.
 Qed.
 Next Obligation.
@@ -56,13 +54,13 @@ Qed.
 Next Obligation.
   rewrite fmap_comp.
   rewrite comp_assoc.
-  srewrite_r (naturality[@Transformation.counit _ _ _ _ A]).
+  srewrite_r (naturality[counit[A]]).
   now rewrite <- comp_assoc.
 Qed.
 
 Program Definition Adjunction_to_Transform {A : F ⊣ U} : F ∹ U := {|
-  Transformation.unit   := {| transform := fun a => @unit _ _ _ _ A a |};
-  Transformation.counit := {| transform := fun b => @counit _ _ _ _ A b |}
+  Transformation.unit   := {| transform := fun _ => unit |};
+  Transformation.counit := {| transform := fun _ => counit |}
 |}.
 Next Obligation.
   unfold unit.

From 16ba1b2a241f9ffcf6859fecb38e39b95c9b991f Mon Sep 17 00:00:00 2001
From: John Wiegley <johnw@newartisans.com>
Date: Tue, 30 Jan 2024 16:22:09 -0800
Subject: [PATCH 12/16] Correct a typo

---
 Adjunction/Natural/Transformation/Universal.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Adjunction/Natural/Transformation/Universal.v b/Adjunction/Natural/Transformation/Universal.v
index 6a1f7d4b..f8364bab 100644
--- a/Adjunction/Natural/Transformation/Universal.v
+++ b/Adjunction/Natural/Transformation/Universal.v
@@ -18,7 +18,7 @@ Context {U : C ⟶ D}.
 
 Program Definition Adjunction_from_Transform (A : F ∹ U) : F ⊣ U := {|
   adj := fun a b =>
-    {| to   := {| morphism := fun f =>n fmap f ∘ transform[unit[A]] a |}
+    {| to   := {| morphism := fun f => fmap f ∘ transform[unit[A]] a |}
      ; from := {| morphism := fun f => transform[counit[A]] b ∘ fmap f |} |}
 |}.
 Next Obligation. proper; now rewrites. Qed.

From 6ceeb6fa22d810d21fba1ecf2afa902c2f3caa66 Mon Sep 17 00:00:00 2001
From: John Wiegley <johnw@newartisans.com>
Date: Tue, 30 Jan 2024 16:38:09 -0800
Subject: [PATCH 13/16] Make some uses explicit

---
 Adjunction/Natural/Transformation/Universal.v | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/Adjunction/Natural/Transformation/Universal.v b/Adjunction/Natural/Transformation/Universal.v
index f8364bab..47bdadf7 100644
--- a/Adjunction/Natural/Transformation/Universal.v
+++ b/Adjunction/Natural/Transformation/Universal.v
@@ -26,21 +26,21 @@ Next Obligation. proper; now rewrites. Qed.
 Next Obligation.
   rewrite fmap_comp.
   rewrite <- comp_assoc.
-  srewrite (naturality[unit[A]]).
-  rewrite comp_assoc.
+  rewrite (@naturality _ _ _ _ unit[A] _ _ x).
+  rewrite comp_assoc; simpl.
   srewrite (@Transformation.fmap_counit_unit); cat.
 Qed.
 Next Obligation.
   rewrite fmap_comp.
   rewrite comp_assoc.
-  srewrite_r (naturality[counit[A]]).
-  rewrite <- comp_assoc.
+  rewrite <- (@naturality _ _ _ _ counit[A] _ _ x).
+  rewrite <- comp_assoc; simpl.
   srewrite (@Transformation.counit_fmap_unit); cat.
 Qed.
 Next Obligation.
   rewrite fmap_comp.
   rewrite <- comp_assoc.
-  srewrite (naturality[unit[A]]).
+  rewrite (@naturality _ _ _ _ unit[A] _ _ g).
   now rewrite comp_assoc.
 Qed.
 Next Obligation.
@@ -54,7 +54,7 @@ Qed.
 Next Obligation.
   rewrite fmap_comp.
   rewrite comp_assoc.
-  srewrite_r (naturality[counit[A]]).
+  rewrite <- (@naturality _ _ _ _ counit[A] _ _ f).
   now rewrite <- comp_assoc.
 Qed.
 

From 4482ec20d83ddb2b09d94d625c978992a32e6aff Mon Sep 17 00:00:00 2001
From: John Wiegley <johnw@newartisans.com>
Date: Tue, 30 Jan 2024 16:46:52 -0800
Subject: [PATCH 14/16] Make more uses explicit

---
 Theory/Kan/Extension.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Theory/Kan/Extension.v b/Theory/Kan/Extension.v
index c2a8f3d6..d7a4027e 100644
--- a/Theory/Kan/Extension.v
+++ b/Theory/Kan/Extension.v
@@ -187,11 +187,11 @@ Proof.
       * simpl.
         rewrite <- to_adj_nat_l.
         rewrite <- to_adj_nat_r.
-        now srewrite (naturality[X0]).
+        now srewrite (@naturality _ _ _ _ X0 _ _ f).
       * simpl.
         rewrite <- to_adj_nat_l.
         rewrite <- to_adj_nat_r.
-        now srewrite (naturality[X0]).
+        now srewrite (@naturality _ _ _ _ X0 _ _ f).
     + simpl.
       proper.
       apply to_adj_respects.
@@ -204,11 +204,11 @@ Proof.
       * simpl.
         rewrite <- from_adj_nat_l.
         rewrite <- from_adj_nat_r.
-        now srewrite (naturality[X0]).
+        now srewrite (@naturality _ _ _ _ X0 _ _ f).
       * simpl.
         rewrite <- from_adj_nat_l.
         rewrite <- from_adj_nat_r.
-        now srewrite (naturality[X0]).
+        now srewrite (@naturality _ _ _ _ X0 _ _ f).
     + simpl.
       proper.
       apply from_adj_respects.

From 284c4bd00b48bfdae4465e6b78c1703bc26eecc0 Mon Sep 17 00:00:00 2001
From: John Wiegley <johnw@newartisans.com>
Date: Tue, 30 Jan 2024 16:57:06 -0800
Subject: [PATCH 15/16] Be more explicit in Hom.v

---
 Adjunction/Hom.v | 24 ++++++++----------------
 1 file changed, 8 insertions(+), 16 deletions(-)

diff --git a/Adjunction/Hom.v b/Adjunction/Hom.v
index 976c2274..09165131 100644
--- a/Adjunction/Hom.v
+++ b/Adjunction/Hom.v
@@ -150,7 +150,7 @@ Qed.
 Next Obligation.
   simpl.
   rewrite <- !comp_assoc.
-  srewrite_r (naturality[unit]).
+  srewrite_r (@naturality _ _ _ _ unit _ _ h).
   rewrite !comp_assoc.
   rewrite <- !fmap_comp.
   reflexivity.
@@ -158,7 +158,7 @@ Qed.
 Next Obligation.
   simpl.
   rewrite <- !comp_assoc.
-  srewrite_r (naturality[unit]).
+  srewrite_r (@naturality _ _ _ _ unit _ _ h).
   rewrite !comp_assoc.
   rewrite <- !fmap_comp.
   reflexivity.
@@ -169,7 +169,7 @@ Qed.
 Next Obligation.
   simpl.
   rewrite !comp_assoc.
-  srewrite (naturality[counit]).
+  srewrite (@naturality _ _ _ _ counit _ _ h0).
   rewrite <- !comp_assoc.
   rewrite <- !fmap_comp.
   reflexivity.
@@ -177,7 +177,7 @@ Qed.
 Next Obligation.
   simpl.
   rewrite !comp_assoc.
-  srewrite (naturality[counit]).
+  srewrite (@naturality _ _ _ _ counit _ _ h0).
   rewrite <- !comp_assoc.
   rewrite <- !fmap_comp.
   reflexivity.
@@ -186,7 +186,7 @@ Next Obligation.
   simpl; cat.
   rewrite fmap_comp.
   rewrite <- comp_assoc.
-  srewrite (naturality[unit]).
+  srewrite (@naturality _ _ _ _ unit _ _ x0).
   rewrite comp_assoc.
   srewrite (@fmap_counit_unit _ _ _ _ A); cat.
 Qed.
@@ -194,7 +194,7 @@ Next Obligation.
   simpl; cat.
   rewrite fmap_comp.
   rewrite comp_assoc.
-  srewrite_r (naturality[counit]).
+  srewrite_r (@naturality _ _ _ _ counit _ _ x0).
   rewrite <- comp_assoc.
   srewrite (@counit_fmap_unit _ _ _ _ A); cat.
 Qed.
@@ -237,14 +237,9 @@ Qed.
 
 Program Definition Adjunction_Universal_to_Hom (A : F ⊣ U) : Adjunction_Hom := {|
   hom_adj :=
-    {| to   := {| transform := fun _ =>
-        {| morphism := fun f => to adj f |} |}
-     ; from := {| transform := fun _ =>
-        {| morphism := fun f => from adj f |} |} |}
+    {| to   := {| transform := fun _ => {| morphism := to adj   |} |}
+     ; from := {| transform := fun _ => {| morphism := from adj |} |} |}
 |}.
-Next Obligation.
-  proper; rewrites; reflexivity.
-Qed.
 Next Obligation.
   rewrite <- comp_assoc.
   rewrite to_adj_nat_l.
@@ -259,9 +254,6 @@ Next Obligation.
   rewrite to_adj_nat_l.
   reflexivity.
 Qed.
-Next Obligation.
-  proper; rewrites; reflexivity.
-Qed.
 Next Obligation.
   rewrite <- comp_assoc.
   rewrite from_adj_nat_l.

From 3fe04f47336c98410cfba4ec9827163e9cd770a8 Mon Sep 17 00:00:00 2001
From: John Wiegley <johnw@newartisans.com>
Date: Tue, 30 Jan 2024 17:10:09 -0800
Subject: [PATCH 16/16] Be more explicit in Functor/Traversable/Product.v

---
 Functor/Traversable/Product.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Functor/Traversable/Product.v b/Functor/Traversable/Product.v
index 03091252..40f0ddb0 100644
--- a/Functor/Traversable/Product.v
+++ b/Functor/Traversable/Product.v
@@ -40,8 +40,8 @@ Proof.
     rewrite comp_assoc.
     rewrites.
     rewrite <- !comp_assoc.
-    pose proof (naturality[@sequence _ _ _ O _ X]) as X3; simpl in *.
-    pose proof (naturality[@sequence _ _ _ P _ X]) as X4; simpl in *.
+    pose proof (naturality[@sequence _ _ _ O _ X] _ _ f) as X3; simpl in *.
+    pose proof (naturality[@sequence _ _ _ P _ X] _ _ f) as X4; simpl in *.
     rewrite !comp_assoc.
     comp_left.
     rewrite bimap_fmap.
@@ -55,8 +55,8 @@ Proof.
     rewrite comp_assoc.
     rewrites.
     rewrite <- !comp_assoc.
-    pose proof (naturality[@sequence _ _ _ O _ X]) as X3; simpl in *.
-    pose proof (naturality[@sequence _ _ _ P _ X]) as X4; simpl in *.
+    pose proof (naturality[@sequence _ _ _ O _ X] _ _ f) as X3; simpl in *.
+    pose proof (naturality[@sequence _ _ _ P _ X] _ _ f) as X4; simpl in *.
     rewrite !comp_assoc.
     comp_left.
     rewrite bimap_fmap.