Merge branch 'master' into ps/rr/biproducts

Author: Alizter

.dir-locals.el

@@ -0,0 +1 @@
+((nil . ((mode . visual-line))))

.github/workflows/ci.yml

@@ -566,28 +566,28 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     # Delete workspace artifacts
-    - uses: geekyeggo/delete-artifact@v1
+    - uses: geekyeggo/delete-artifact@v5
       with:
         name: workspace-${{ env.coq-version-supported }}
-    - uses: geekyeggo/delete-artifact@v1
+    - uses: geekyeggo/delete-artifact@v5
       with:
         name: workspace-latest
-    - uses: geekyeggo/delete-artifact@v1
+    - uses: geekyeggo/delete-artifact@v5
       with:
         name: workspace-dev
     # Delete documentation artifacts
-    - uses: geekyeggo/delete-artifact@v1
+    - uses: geekyeggo/delete-artifact@v5
       with:
         name: dep-graphs
-    - uses: geekyeggo/delete-artifact@v1
+    - uses: geekyeggo/delete-artifact@v5
       with:
         name: file-dep-graphs
-    - uses: geekyeggo/delete-artifact@v1
+    - uses: geekyeggo/delete-artifact@v5
       with:
         name: alectryon-html
-    - uses: geekyeggo/delete-artifact@v1
+    - uses: geekyeggo/delete-artifact@v5
       with:
         name: coqdoc-html
-    - uses: geekyeggo/delete-artifact@v1
+    - uses: geekyeggo/delete-artifact@v5
       with:
         name: timing-html

STYLE.md

@@ -390,7 +390,7 @@ Definition Book_3_3_1 := fun A => @HoTT.Basics.Overture.IsTrunc (-1) A.
 (* ================================================== thm:inhabprop-eqvunit *)
 (** Lemma 3.3.2 *)
 
-Definition Book_3_3_2 := @HoTT.HProp.if_hprop_then_equiv_Unit.
+Definition Book_3_3_2 := @HoTT.Universes.HProp.if_hprop_then_equiv_Unit.
 
 (* ================================================== lem:equiv-iff-hprop *)
 (** Lemma 3.3.3 *)
@@ -694,12 +694,12 @@ Definition Book_4_8_2 := @HoTT.HFiber.equiv_fibration_replacement.
 (* ================================================== thm:nobject-classifier-appetizer *)
 (** Theorem 4.8.3 *)
 
-Definition Book_4_8_3 := @HoTT.ObjectClassifier.equiv_sigma_fibration.
+Definition Book_4_8_3 := @HoTT.Universes.ObjectClassifier.equiv_sigma_fibration.
 
 (* ================================================== thm:object-classifier *)
 (** Theorem 4.8.4 *)
 
-Definition Book_4_8_4 := @HoTT.ObjectClassifier.ispullback_objectclassifier_square.
+Definition Book_4_8_4 := @HoTT.Universes.ObjectClassifier.ispullback_objectclassifier_square.
 
 (* ================================================== weakfunext *)
 (** Definition 4.9.1 *)
@@ -1000,7 +1000,7 @@ Definition Book_7_1_9 := @HoTT.Basics.Trunc.istrunc_forall.
 (* ================================================== thm:hleveln-of-hlevelSn *)
 (** Theorem 7.1.11 *)
 
-Definition Book7_1_11 := @HoTT.TruncType.istrunc_trunctype.
+Definition Book7_1_11 := @HoTT.Universes.TruncType.istrunc_trunctype.
 
 (* ================================================== thm:h-set-uip-K *)
 (** Theorem 7.2.1 *)
@@ -1010,7 +1010,7 @@ Definition Book7_1_11 := @HoTT.TruncType.istrunc_trunctype.
 (* ================================================== thm:h-set-refrel-in-paths-sets *)
 (** Theorem 7.2.2 *)
 
-Definition Book_7_2_2 := @HoTT.HSet.ishset_hrel_subpaths.
+Definition Book_7_2_2 := @HoTT.Universes.HSet.ishset_hrel_subpaths.
 
 (* ================================================== notnotstable-equality-to-set *)
 (** Corollary 7.2.3 *)

contrib/HoTTBook.v

@@ -803,7 +803,7 @@ Defined.
 (* ================================================== ex:prop-inhabcontr *)
 (** Exercise 3.5 *)
 
-Definition Book_3_5_solution_1 := @HoTT.HProp.equiv_hprop_inhabited_contr.
+Definition Book_3_5_solution_1 := @HoTT.Universes.HProp.equiv_hprop_inhabited_contr.
 
 (* ================================================== ex:lem-mereprop *)
 (** Exercise 3.6 *)
@@ -1712,7 +1712,7 @@ End Book_6_9.
 Section Book_7_1.
   Lemma Book_7_1_part_i (H : forall A, merely A -> A) A : IsHSet A.
   Proof.
-    apply (@HoTT.HSet.ishset_hrel_subpaths
+    apply (@HoTT.Universes.HSet.ishset_hrel_subpaths
              A (fun x y => merely (x = y)));
     try typeclasses eauto.
     - intros ?.

contrib/HoTTBookExercises.v

@@ -1,5 +1,3 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
-
 (* Typeclass instances to allow rewriting in categories. Examples are given later in the file. *)
 
 (* Init.Tactics contains the definition of the Coq stdlib typeclass_inferences database. It must be imported before Basics.Overture. *)
@@ -10,9 +8,11 @@ All files that import WildCat/SetoidRewrite.v will also recursively import the e
 
 (** Because of this, this file needs to be the *first* file Require'd in any file that uses it.  Otherwise, the typeclasses hintdb is cleared, breaking typeclass inference.  Moreover, if Foo Requires this file, then Foo must also be the first file Require'd in any file that Requires Foo, and so on. In the long term it would be good if this could be avoided.*)
 
+#[warnings="-deprecated-from-Coq"]
 From Coq Require Init.Tactics.
 From HoTT Require Import Basics.Overture Basics.Tactics.
 From HoTT Require Import Types.Forall.
+#[warnings="-deprecated-from-Coq"]
 From Coq Require Setoids.Setoid.
 Import CMorphisms.ProperNotations.
 From HoTT Require Import WildCat.Core

contrib/SetoidRewrite.v

@@ -29,7 +29,8 @@
           useDune = true;
         };
 
-        devShells.default = makeDevShell { coq = pkgs.coq_8_19; } { };
+        devShells.default = makeDevShell { coq = pkgs.coq_8_20; } { };
+        devShells.coq_8_19 = makeDevShell { coq = pkgs.coq_8_19; } { };
 
         # To use, pass --impure to nix develop
         devShells.coq_master =

flake.lock

@@ -1,4 +1,4 @@
-From HoTT Require Import Basics Types DProp Tactics.EquivalenceInduction.
+From HoTT Require Import Basics Types Universes.DProp Tactics.EquivalenceInduction.
 
 Local Open Scope nat_scope.
 

flake.nix

@@ -29,6 +29,28 @@ Proof.
   split; exact _.
 Defined.
 
+(** Easier way to build abelian groups without redundant information. *)
+Definition Build_AbGroup' (G : Type)
+  `{Zero G, Negate G, Plus G, IsHSet G}
+  (comm : Commutative (A:=G) (+))
+  (assoc : Associative (A:=G) (+))
+  (unit_l : LeftIdentity (A:=G) (+) 0)
+  (inv_l : LeftInverse (A:=G) (+) (-) 0)
+  : AbGroup.
+Proof.
+  snrapply Build_AbGroup.
+  - (* TODO: introduce smart constructor for [Build_Group] *)
+    rapply (Build_Group G).
+    repeat split; only 1-3, 5: exact _.
+    + intros x.
+      lhs nrapply comm.
+      exact (unit_l x).
+    + intros x.
+      lhs nrapply comm.
+      exact (inv_l x).
+  - exact comm.
+Defined.
+
 Definition issig_abgroup : _ <~> AbGroup := ltac:(issig).
 
 Global Instance zero_abgroup (A : AbGroup) : Zero A := group_unit.
@@ -91,11 +113,7 @@ Global Instance isabgroup_quotient (G : AbGroup) (H : Subgroup G)
 Proof.
   nrapply Build_IsAbGroup.
   1: exact _.
-  intro x.
-  srapply Quotient_ind_hprop.
-  intro y; revert x.
-  srapply Quotient_ind_hprop.
-  intro x.
+  srapply Quotient_ind2_hprop; intros x y.
   apply (ap (class_of _)).
   apply commutativity.
 Defined.

test/bugs/github754.v

@@ -164,7 +164,7 @@ End Abel.
 (** The [IsHProp] argument of [Abel_ind_hprop] can usually be found by typeclass resolution, but [srapply] is slow, so we use this tactic instead. *)
 Local Ltac Abel_ind_hprop x := snrapply Abel_ind_hprop; [exact _ | intro x].
 
-(** We make sure that G is implicit in the arguments of [abel_in
+(** We make sure that [G] is implicit in the arguments of [abel_in]
  and [abel_in_comm]. *)
 Arguments abel_in {_}.
 Arguments abel_in_comm {_}.
@@ -176,9 +176,9 @@ Section AbelGroup.
   Context (G : Group).
 
   (** Firstly we derive the operation on Abel G. This is defined as follows:
-      <<
+<<
         abel_in x + abel_in y := abel_in (x * y)
-      >>
+>>
       But we need to also check that it preserves ab_comm in the appropriate way. *)
   Global Instance abel_sgop : SgOp (Abel G).
   Proof.
@@ -251,13 +251,13 @@ Section AbelGroup.
   Defined.
 
   (** Now we can define the negation. This is just
-      <<
+<<
         - (abel_in g) := abel_in (- g)
-      >>
+>>
       However when checking that it respects ab_comm we have to show the following:
-      <<
+<<
         abel_in (- z * - y * - x) = abel_in (- y * - z * - x)
-      >>
+>>
       there is no obvious way to do this, but we note that [abel_in (x * y)] is exactly the definition of [abel_in x + abel_in y]! Hence by commutativity we can show this. *)
   Global Instance abel_negate : Negate (Abel G).
   Proof.

theories/Algebra/AbGroups/AbelianGroup.v

@@ -138,10 +138,6 @@ Definition ab_biprod_corec {A B X : AbGroup} (f : X $-> A) (g : X $-> B)
   : X $-> ab_biprod A B
   := grp_prod_corec f g.
 
-Definition ab_corec_eta {X Y A B : AbGroup} (f : X $-> Y) (g0 : Y $-> A) (g1 : Y $-> B)
-  : ab_biprod_corec g0 g1 $o f $== ab_biprod_corec (g0 $o f) (g1 $o f)
-  := fun _ => idpath.
-
 (** *** Functoriality of [ab_biprod] *)
 
 Definition functor_ab_biprod {A A' B B' : AbGroup} (f : A $-> A') (g: B $-> B')

theories/Algebra/AbGroups/Abelianization.v

@@ -12,14 +12,16 @@ Local Open Scope int_scope.
 
 Definition abgroup_Z@{} : AbGroup@{Set}.
 Proof.
-  snrapply Build_AbGroup.
-  - refine (Build_Group Int int_add 0 int_neg _); repeat split.
-    + exact _.
-    + exact int_add_assoc.
-    + exact int_add_0_r.
-    + exact int_add_neg_l.
-    + exact int_add_neg_r.
+  snrapply Build_AbGroup'.
+  - exact Int.
+  - exact 0.
+  - exact int_neg.
+  - exact int_add.
+  - exact _.
   - exact int_add_comm.
+  - exact int_add_assoc.
+  - exact int_add_0_l.
+  - exact int_add_neg_l.
 Defined.
 
 (** For every group [G] and element [g : G], the map sending an integer to that power of [g] is a homomorphism.  See [ab_mul] for the homomorphism [G -> G] when [G] is abelian. *)

theories/Algebra/AbGroups/Biproduct.v

@@ -625,11 +625,17 @@ Proposition projection_split_beta {B A : AbGroup} (E : AbSES B A)
   : projection_split_iso E h o (inclusion _) == ab_biprod_inl.
 Proof.
   intro a.
-  refine (ap _ (ab_corec_eta _ _ _ _) @ _).
-  refine (ab_biprod_functor_beta _ _ _ _ _ @ _).
+  (* The next two lines might help the reader, but both are definitional equalities:
+  lhs nrapply (ap _ (grp_prod_corec_natural _ _ _ _)).
+  lhs nrapply ab_biprod_functor_beta.
+  *)
   nrapply path_prod'.
   2: rapply cx_isexact.
-  refine (ap _ (projection_split_to_kernel_beta E h a) @ _).
+  (* The LHS of the remaining goal is definitionally equal to
+       (grp_iso_inverse (grp_iso_cxfib (isexact_inclusion_projection E)) $o
+         (projection_split_to_kernel E h $o inclusion E)) a
+     allowing us to do: *)
+  lhs nrapply (ap _ (projection_split_to_kernel_beta E h a)).
   apply eissect.
 Defined.
 
@@ -731,8 +737,7 @@ Proof.
   - apply isequiv_surj_emb.
     1: rapply cancelR_conn_map.
     apply isembedding_isinj_hset.
-    srapply Quotient_ind_hprop; intro x.
-    srapply Quotient_ind_hprop; intro y.
+    srapply Quotient_ind2_hprop; intros x y.
     intro p.
     apply qglue; cbn.
     refine (isexact_preimage (Tr (-1)) _ _ (-x + y) _).

theories/Algebra/AbGroups/Z.v

@@ -1,8 +1,7 @@
-(* -*- mode: coq; mode: visual-line -*-  *)
 Require Import Basics.
 Require Import Truncations.
 Require Import Algebra.ooGroup.
-Require Import Spaces.BAut.
+Require Import Universes.BAut.
 Require Import Pointed.Core.
 
 Local Open Scope pointed_scope.

theories/Algebra/AbSES/Core.v

@@ -831,20 +831,24 @@ Proof.
 Defined.
 
 (** Maps into the direct product can be built by mapping separately into each factor. *)
-Proposition grp_prod_corec {G H K : Group}
-            (f : GroupHomomorphism K G)
-            (g : GroupHomomorphism K H)
-  : GroupHomomorphism K (grp_prod G H).
+Proposition grp_prod_corec {G H K : Group} (f : K $-> G) (g : K $-> H)
+  : K $-> (grp_prod G H).
 Proof.
   snrapply Build_GroupHomomorphism.
-  - exact (fun x:K => (f x, g x)).
+  - exact (fun x : K => (f x, g x)).
   - intros x y.
-    refine (path_prod' _ _ ); try apply grp_homo_op.
+    apply path_prod'; apply grp_homo_op.
 Defined.
 
+(** [grp_prod_corec] satisfies a definitional naturality property. *)
+Definition grp_prod_corec_natural {X Y A B : Group}
+  (f : X $-> Y) (g0 : Y $-> A) (g1 : Y $-> B)
+  : grp_prod_corec g0 g1 $o f $== grp_prod_corec (g0 $o f) (g1 $o f)
+  := fun _ => idpath.
+
 (** The left factor injects into the direct product. *)
 Definition grp_prod_inl {H K : Group}
-  : GroupHomomorphism H (grp_prod H K)
+  : H $-> (grp_prod H K)
   := grp_prod_corec grp_homo_id grp_homo_const.
 
 (** The left injection is an embedding. *)
@@ -858,7 +862,7 @@ Defined.
 
 (** The right factor injects into the direct product. *)
 Definition grp_prod_inr {H K : Group}
-  : GroupHomomorphism K (grp_prod H K)
+  : K $-> (grp_prod H K)
   := grp_prod_corec grp_homo_const grp_homo_id.
 
 (** The right injection is an embedding. *)

theories/Algebra/Aut.v

@@ -27,23 +27,11 @@ Section GroupCongruenceQuotient.
 
   Global Instance congquot_sgop : SgOp CongruenceQuotient.
   Proof.
-    intros x.
-    srapply Quotient_rec.
-    { intro y; revert x.
-      srapply Quotient_rec.
-      { intros x.
-        apply class_of.
-        exact (x * y). }
-      intros a b r.
-      cbn.
-      apply qglue.
-      by apply iscong. }
-    intros a b r.
-    revert x.
-    srapply Quotient_ind_hprop.
-    intro x.
-    apply qglue.
-    by apply iscong.
+    srapply Quotient_rec2.
+    - intros x y.
+      exact (class_of _ (x * y)).
+    - intros x x' y p. apply qglue. by apply iscong.
+    - intros x y y' q. apply qglue. by apply iscong.
   Defined.
 
   Global Instance congquot_mon_unit : MonUnit CongruenceQuotient.
@@ -72,10 +60,7 @@ Section GroupCongruenceQuotient.
 
   Global Instance congquot_sgop_associative : Associative congquot_sgop.
   Proof.
-    intros x y.
-    srapply Quotient_ind_hprop; intro a; revert y.
-    srapply Quotient_ind_hprop; intro b; revert x.
-    srapply Quotient_ind_hprop; intro c.
+    srapply Quotient_ind3_hprop; intros x y z.
     simpl; by rewrite associativity.
   Qed.