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 01/15] 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 02/15] 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 03/15] 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 04/15] 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 05/15] 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 06/15] 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 07/15] 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 08/15] 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 09/15] 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 10/15] 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 11/15] 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 12/15] 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 13/15] 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 14/15] 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 15/15] 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.