Merge remote-tracking branch 'origin/master' into coq-8.17

jwiegley · Jan 31, 2024 · 3bfc550 · 3bfc550
2 parents 2aaea15 + 5ff107d
commit 3bfc550
Show file tree

Hide file tree

Showing 10 changed files with 60 additions and 77 deletions.
diff --git 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/Adjunction/Hom.v b/Adjunction/Hom.v
@@ -150,15 +150,15 @@ Qed.
 Next Obligation.
   simpl.
   rewrite <- !comp_assoc.
-  srewrite_r (naturality[unit]).
+  srewrite_r (@naturality _ _ _ _ unit _ _ h).
   rewrite !comp_assoc.
   rewrite <- !fmap_comp.
   reflexivity.
 Qed.
 Next Obligation.
   simpl.
   rewrite <- !comp_assoc.
-  srewrite_r (naturality[unit]).
+  srewrite_r (@naturality _ _ _ _ unit _ _ h).
   rewrite !comp_assoc.
   rewrite <- !fmap_comp.
   reflexivity.
@@ -169,15 +169,15 @@ Qed.
 Next Obligation.
   simpl.
   rewrite !comp_assoc.
-  srewrite (naturality[counit]).
+  srewrite (@naturality _ _ _ _ counit _ _ h0).
   rewrite <- !comp_assoc.
   rewrite <- !fmap_comp.
   reflexivity.
 Qed.
 Next Obligation.
   simpl.
   rewrite !comp_assoc.
-  srewrite (naturality[counit]).
+  srewrite (@naturality _ _ _ _ counit _ _ h0).
   rewrite <- !comp_assoc.
   rewrite <- !fmap_comp.
   reflexivity.
@@ -186,15 +186,15 @@ 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.
 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.

diff --git a/Adjunction/Natural/Transformation/Universal.v b/Adjunction/Natural/Transformation/Universal.v
@@ -18,55 +18,49 @@ 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 => fmap f ∘ transform[unit[A]] a |}
+     ; from := {| morphism := fun f => transform[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]).
-  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[Transformation.counit]).
-  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[Transformation.unit]).
-  rewrite comp_assoc.
-  reflexivity.
+  rewrite (@naturality _ _ _ _ unit[A] _ _ g).
+  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.
+  rewrite <- (@naturality _ _ _ _ counit[A] _ _ f).
+  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.

diff --git 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.

diff --git a/Monad/Adjunction.v b/Monad/Adjunction.v
@@ -75,7 +75,9 @@ Proof.
   - simpl.
     srewrite (@fmap_counit_unit); cat.
   - rewrite <- !fmap_comp.
-    srewrite (naturality[counit]); cat.
+    apply fmap_respects.
+    symmetry.
+    apply (naturality[counit]).
 Qed.
 
 End AdjunctionMonad.
diff --git 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.
@@ -201,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.
@@ -218,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.

diff --git 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).

diff --git 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:dev bash -c '
     git clone https://github.com/jwiegley/category-theory;
     cd category-theory;
     opam update;

diff --git 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")}
 ]
 

diff --git 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;
 }