Merge branch 'master' into ps/rr/tensor_preserves_coequalizers

.github/workflows/ci.yml

@@ -133,7 +133,7 @@ jobs:
           endGroup
           echo "::remove-matcher owner=coq-problem-matcher::" # remove problem matcher installed by Coq docker action, so we don't get duplicate warning annotations
           sudo apt-get -o Acquire::Retries=30 update -q
-          sudo apt-get -o Acquire::Retries=30 install python -y --allow-unauthenticated
+          sudo apt-get -o Acquire::Retries=30 install python3 python-is-python3 -y --allow-unauthenticated
           etc/coq-scripts/github/reportify-coq.sh --errors ${{ matrix.extra-gh-reportify }} make TIMED=1 -j2 --output-sync
 
     - name: Revert permissions
@@ -202,11 +202,16 @@ jobs:
         custom_script: |
           opam install -y coq-serapi
           sudo apt-get -o Acquire::Retries=30 update -q
-          sudo apt-get -o Acquire::Retries=30 install python3-pip autoconf -y --allow-unauthenticated
-          python3 -m pip install --user --upgrade pygments dominate beautifulsoup4 docutils==0.17.1
+          sudo apt-get -o Acquire::Retries=30 install python3-pip python3-venv autoconf -y --allow-unauthenticated
           startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
             sudo chown -R coq:coq .
           endGroup
+          # Create and activate a virtual environment
+          python3 -m venv myenv
+          source myenv/bin/activate
+          # Install the required Python packages in the virtual environment
+          python -m pip install --upgrade pip
+          python -m pip install pygments dominate beautifulsoup4 docutils==0.17.1
           echo "::remove-matcher owner=coq-problem-matcher::" # remove problem matcher installed by Coq docker action, so we don't get duplicate warning annotations
           make alectryon ALECTRYON_EXTRAFLAGS=--traceback
     - name: Revert permissions
@@ -375,7 +380,7 @@ jobs:
         ocaml_version: ${{ env.ocaml-version }}
         custom_script: |
           sudo apt-get update
-          sudo apt-get install -y time python lua5.1
+          sudo apt-get install -y time python3 python-is-python3 lua5.1
           startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
             sudo chown -R coq:coq .
           endGroup

contrib/HoTTBook.v

@@ -345,7 +345,7 @@ Definition Book_3_1_3 := @HoTT.Types.Empty.istrunc_Empty (-2).
 (* ================================================== thm:nat-set *)
 (** Example 3.1.4 *)
 
-Definition Book_3_1_4 := @HoTT.Spaces.Nat.Core.hset_nat.
+Definition Book_3_1_4 := @HoTT.Spaces.Nat.Core.ishset_nat.
 
 (* ================================================== thm:isset-prod *)
 (** Example 3.1.5 *)

contrib/HoTTBookExercises.v

@@ -1169,7 +1169,7 @@ End Book_4_5.
 Section Book_4_6_i.
 
   Definition is_qinv {A B : Type} (f : A -> B)
-    := { g : B -> A & ((f o g == idmap) * (g o f == idmap))%type }.
+    := { g : B -> A & (f o g == idmap) * (g o f == idmap) }.
   Definition qinv (A B : Type)
     := { f : A -> B & is_qinv f }.
   Definition qinv_id A : qinv A A

test/Algebra/Groups/Presentation.v

@@ -1,4 +1,5 @@
-From HoTT.Algebra.Groups Require Import Group Presentation.
+From HoTT Require Import Basics Spaces.Finite.Fin Spaces.Finite.FinSeq.
+From HoTT.Algebra.Groups Require Import Group Presentation FreeGroup.
 
 Local Open Scope mc_scope.
 Local Open Scope mc_mult_scope.

theories/Algebra/AbGroups/AbelianGroup.v

@@ -80,11 +80,8 @@ Coercion abgroup_subgroup : Subgroup >-> AbGroup.
 Global Instance isnormal_ab_subgroup (G : AbGroup) (H : Subgroup G)
   : IsNormalSubgroup H.
 Proof.
-  intros x y; unfold in_cosetL, in_cosetR.
-  refine (_ oE equiv_subgroup_inverse _ _).
-  rewrite negate_sg_op.
-  rewrite negate_involutive.
-  by rewrite (commutativity (-y) x).
+  intros x y h.
+  by rewrite ab_comm.
 Defined.
 
 (** ** Quotients of abelian groups *)
@@ -305,9 +302,7 @@ Proof.
   - exact zero.
   - refine (f n _ + IHn _).
     intros k Hk.
-    refine (f k _).
-    apply leq_S.
-    exact Hk.
+    exact (f k _).
 Defined.
 
 (** If the function is constant in the range of a finite sum then the sum is equal to the constant times [n]. This is a group power in the underlying group. *)
@@ -317,7 +312,7 @@ Definition ab_sum_const {A : AbGroup} (n : nat) (a : A)
 Proof.
   induction n as [|n IHn] in f, p |- *.
   - reflexivity.
-  - rhs nrapply (ap@{Set _} _ (int_of_nat_succ_commute n)).
+  - rhs_V nrapply (ap@{Set _} _ (int_nat_succ n)).
     rhs nrapply grp_pow_succ.
     simpl. f_ap.
     apply IHn.

theories/Algebra/AbGroups/Abelianization.v

@@ -145,8 +145,9 @@ Section Abel.
     (a : forall x, P (abel_in x))
     : forall (x : Abel), P x.
   Proof.
-    srapply (Abel_ind _ a).
-    intros; apply path_ishprop.
+    srapply Trunc_ind.
+    srapply Coeq_ind_hprop.
+    exact a.
   Defined.
 
   (** And its recursion version. *)

theories/Algebra/AbGroups/Cyclic.v

@@ -1,80 +1,18 @@
-Require Import Basics Types WildCat.Core Truncations.Core
-  AbelianGroup AbHom Centralizer AbProjective
-  Groups.FreeGroup AbGroups.Z Spaces.Int.
+Require Import Basics.Overture Basics.Tactics WildCat.Core AbelianGroup
+  AbGroups.Z Spaces.Int Groups.QuotientGroup.
 
 (** * Cyclic groups *)
 
-(** ** The free group on one generator *)
+(** The [n]-th cyclic group is the cokernel of [ab_mul n]. *)
+Definition cyclic (n : nat) : AbGroup
+  := ab_cokernel (ab_mul (A:=abgroup_Z) n).
 
-(** We can define the integers as the free group on one generator, which we denote [Z1] below. Results from Centralizer.v and Groups.FreeGroup let us show that [Z1] is abelian. *)
+Definition cyclic_in (n : nat) : abgroup_Z $-> cyclic n
+  := grp_quotient_map. 
 
-(** We define [Z] as the free group with a single generator. *)
-Definition Z1 := FreeGroup Unit.
-Definition Z1_gen : Z1 := freegroup_in tt. (* The generator *)
-
-(** The recursion principle of [Z1] and its computation rule. *)
-Definition Z1_rec {G : Group@{u}} (g : G) : Z1 $-> G
-  := FreeGroup_rec Unit G (unit_name g).
-
-Definition Z1_rec_beta {G : Group} (g : G) : Z1_rec g Z1_gen = g
-  := FreeGroup_rec_beta _ _ _.
-
-(** The free group [Z] on one generator is isomorphic to the subgroup of [Z] generated by the generator.  And such cyclic subgroups are known to be commutative, by [commutative_cyclic_subgroup]. *)
-Global Instance Z1_commutative `{Funext} : Commutative (@group_sgop Z1)
-  := commutative_iso_commutative iso_subgroup_incl_freegroupon.
-(* TODO: [Funext] is used in [isfreegroupon_freegroup], but there is a comment there saying that it can be removed.  If that is done, can remove it from many results in this file. A different proof of this result, directly using the construction of the free group, could probably also avoid [Funext]. *)
-
-Definition ab_Z1 `{Funext} : AbGroup
-  := Build_AbGroup Z1 _.
-
-(** The universal property of [ab_Z1]. *)
-Lemma equiv_Z1_hom@{u v | u < v} `{Funext} (A : AbGroup@{u})
-  : GroupIsomorphism (ab_hom@{u v} ab_Z1@{u v} A) A.
+Definition ab_mul_cyclic_in (n : nat) (x y : abgroup_Z)
+  : ab_mul y (cyclic_in n x) = cyclic_in n (y * x)%int.
 Proof.
-  snrapply Build_GroupIsomorphism'.
-  - refine (_ oE (equiv_freegroup_rec@{u u u v} A Unit)^-1).
-    symmetry. refine (Build_Equiv _ _ (fun a => unit_name a) _).
-  - intros f g. cbn. reflexivity.
+  lhs_V nrapply ab_mul_natural.
+  apply ap, abgroup_Z_ab_mul.
 Defined.
-
-Definition nat_to_Z1 : nat -> Z1
-  := fun n => grp_pow Z1_gen n.
-
-Definition Z1_mul_nat `{Funext} (n : nat) : ab_Z1 $-> ab_Z1
-  := Z1_rec (nat_to_Z1 n).
-
-Lemma Z1_mul_nat_beta {A : AbGroup} (a : A) (n : nat)
-  : Z1_rec a (nat_to_Z1 n) = ab_mul n a.
-Proof.
-  induction n as [|n H].
-  1: easy.
-  exact (grp_pow_natural _ _ _).
-Defined.
-
-(** [ab_Z1] is projective. *)
-Global Instance ab_Z1_projective `{Funext}
-  : IsAbProjective ab_Z1.
-Proof.
-  intros A B p f H1.
-  pose proof (a := @center _ (H1 (f Z1_gen))).
-  strip_truncations.
-  snrefine (tr (Z1_rec a.1; _)).
-  cbn beta. apply ap10.
-  apply ap. (* of the coercion [grp_homo_map] *)
-  apply path_homomorphism_from_free_group.
-  simpl.
-  intros [].
-  exact a.2.
-Defined.
-
-(** The map sending the generator to [1 : Int]. *)
-Definition Z1_to_Z `{Funext} : ab_Z1 $-> abgroup_Z
-  := Z1_rec (G:=abgroup_Z) 1%int.
-
-(** TODO:  Prove that [Z1_to_Z] is a group isomorphism. *)
-
-(** * Finite cyclic groups *)
-
-(** The [n]-th cyclic group is the cokernel of [Z1_mul_nat n]. *)
-Definition cyclic@{u v | u < v} `{Funext} (n : nat) : AbGroup@{u}
-  := ab_cokernel@{u v} (Z1_mul_nat n).

theories/Algebra/AbSES/SixTerm.v

@@ -1,6 +1,6 @@
 Require Import Basics Types WildCat HSet Pointed.Core Pointed.pTrunc Pointed.pEquiv
   Modalities.ReflectiveSubuniverse Truncations.Core Truncations.SeparatedTrunc
-  AbGroups Homotopy.ExactSequence Spaces.Int
+  AbGroups Homotopy.ExactSequence Spaces.Int Spaces.FreeInt
   AbSES.Core AbSES.Pullback AbSES.Pushout BaerSum Ext PullbackFiberSequence.
 
 (** * The contravariant six-term sequence of Ext *)

theories/Algebra/Groups/FreeGroup.v

@@ -91,8 +91,7 @@ Section Reduction.
       nrapply (freegroup_tau _ a). }
     intros [[c b] d].
     revert y.
-    snrapply Coeq_ind. (* TODO: create and use Coeq_ind_hprop *)
-    2: intro; rapply path_ishprop. 
+    srapply Coeq_ind_hprop.
     intro a.
     change (freegroup_eta ((c ++ [b] ++ [b^] ++ d) ++ a)
       = freegroup_eta ((c ++ d) ++ a)).
@@ -198,9 +197,9 @@ Section Reduction.
   Proof.
     intros x y z.
     strip_truncations.
-    revert x; snrapply Coeq_ind; intro x; [ | apply path_ishprop].
-    revert y; snrapply Coeq_ind; intro y; [ | apply path_ishprop].
-    revert z; snrapply Coeq_ind; intro z; [ | apply path_ishprop].
+    revert x; srapply Coeq_ind_hprop; intro x.
+    revert y; srapply Coeq_ind_hprop; intro y.
+    revert z; srapply Coeq_ind_hprop; intro z.
     nrapply (ap (tr o coeq)).
     nrapply app_assoc.
   Defined.
@@ -209,15 +208,15 @@ Section Reduction.
   Global Instance leftidentity_freegroup_type : LeftIdentity sg_op mon_unit.
   Proof.
     rapply Trunc_ind.
-    srapply Coeq_ind; intro x; [ | apply path_ishprop].
+    srapply Coeq_ind_hprop; intros x.
     reflexivity.
   Defined.
 
   (** Right identity *)
   Global Instance rightidentity_freegroup_type : RightIdentity sg_op mon_unit.
   Proof.
     rapply Trunc_ind.
-    srapply Coeq_ind; intro x; [ | apply path_ishprop].
+    srapply Coeq_ind_hprop; intros x.
     apply (ap tr), ap.
     nrapply app_nil.
   Defined.
@@ -226,15 +225,15 @@ Section Reduction.
   Global Instance leftinverse_freegroup_type : LeftInverse sg_op negate mon_unit.
   Proof.
     rapply Trunc_ind.
-    srapply Coeq_ind; intro x; [ | apply path_ishprop].
+    srapply Coeq_ind_hprop; intro x.
     apply word_concat_Vw.
   Defined.
 
   (** Right inverse *)
   Global Instance rightinverse_freegroup_type : RightInverse sg_op negate mon_unit.
   Proof.
     rapply Trunc_ind.
-    srapply Coeq_ind; intro x; [ | apply path_ishprop].
+    srapply Coeq_ind_hprop; intro x.
     apply word_concat_wV.
   Defined.
 
@@ -313,8 +312,8 @@ Section Reduction.
       intros [[b a] c].
       apply words_rec_coh. }
     intros x y; strip_truncations.
-    revert x; snrapply Coeq_ind; hnf; intro x; [ | apply path_ishprop ].
-    revert y; snrapply Coeq_ind; hnf; intro y; [ | apply path_ishprop ].
+    revert x; srapply Coeq_ind_hprop; intro x.
+    revert y; srapply Coeq_ind_hprop; intro y. 
     simpl.
     apply words_rec_pp.
   Defined.
@@ -334,9 +333,8 @@ Section Reduction.
     : forall x, P x.
   Proof.
     rapply Trunc_ind.
-    snrapply Coeq_ind.
-    - exact H1.
-    - intro; apply path_ishprop.
+    srapply Coeq_ind_hprop.
+    exact H1.
   Defined.
 
   Definition FreeGroup_ind_hprop (P : FreeGroup -> Type)

theories/Algebra/Groups/Group.v

@@ -983,3 +983,16 @@ Proof.
   rhs nrapply grp_homo_op.
   exact (ap011 _ p q).
 Defined.
+
+(** The group movement lemmas can be extended to when there is a homomorphism involved.  For now, we only include these two. *)
+Definition grp_homo_moveL_1V {A B : Group} (f : GroupHomomorphism A B) (x y : A)
+  : f (x * y) = group_unit <~> (f x = - f y)
+  := grp_moveL_1V oE equiv_concat_l (grp_homo_op f x y)^ _.
+
+Definition grp_homo_moveL_1M  {A B : Group} (f : GroupHomomorphism A B) (x y : A)
+  : f (x * -y) = group_unit <~> (f x = f y).
+Proof.
+  refine (grp_moveL_1M oE equiv_concat_l _^ _).
+  lhs nrapply grp_homo_op.
+  apply ap, grp_homo_inv.
+Defined.

theories/Algebra/Groups/GroupCoeq.v

@@ -34,8 +34,7 @@ Proof.
     refine (p _ @ _).
     revert x.
     rapply Trunc_ind.
-    srapply Coeq_ind.
-    2: intros; apply path_ishprop.
+    srapply Coeq_ind_hprop.
     intros w. hnf.
     induction w.
     1: apply ap, grp_homo_unit.

theories/Algebra/Groups/Kernel.v

@@ -11,19 +11,17 @@ Local Open Scope mc_mult_scope.
 Definition grp_kernel {A B : Group} (f : GroupHomomorphism A B) : NormalSubgroup A.
 Proof.
   snrapply Build_NormalSubgroup.
-  - srapply (Build_Subgroup' (fun x => f x = group_unit)).
+  - srapply (Build_Subgroup' (fun x => f x = group_unit)); cbn beta.
     1: apply grp_homo_unit.
-    intros x y p q; cbn in p, q; cbn.
-    refine (grp_homo_op _ _ _ @ ap011 _ p _ @ _).
-    1: apply grp_homo_inv.
-    rewrite q; apply right_inverse.
-  - intros x y; cbn.
-    rewrite 2 grp_homo_op.
-    rewrite 2 grp_homo_inv.
-    refine (_^-1 oE grp_moveL_M1).
-    refine (_ oE equiv_path_inverse _ _).
-    apply grp_moveR_1M.
-  Defined.
+    intros x y p q.
+    apply (grp_homo_moveL_1M _ _ _)^-1.
+    exact (p @ q^).
+  - intros x y; cbn; intros p.
+    apply (grp_homo_moveL_1V _ _ _)^-1.
+    lhs_V nrapply grp_inv_inv.
+    apply (ap (-)).
+    exact ((grp_homo_moveL_1V f x y) p)^.
+Defined.
 
 (** ** Corecursion principle for group kernels *)