Merge branch 'master' into ps/rr/associativity_of_ideal_product

STYLE.md

@@ -111,7 +111,7 @@ corresponding file `Foo.v` that imports everything in the subdirectory.
 
 - There are files in the root `theories/` directory, including
   `EquivGroupoids`, `ExcludedMiddle`, `Factorization`, `HFiber`,
-  `Extensions`, `NullHomotopy`, `PathAny`, `Projective`,
+  `Extensions`, `NullHomotopy`, `Projective`,
   `Idempotents`, `Constant`, `BoundedSearch`, etc.  These contain more
   advanced results which may depend on files in the whole library.  We
   try to limit the number of files in the top-level folder, and would
@@ -160,6 +160,8 @@ corresponding file `Foo.v` that imports everything in the subdirectory.
   and `Spaces/No/*` (the surreal numbers),
 
 - `Homotopy/*`: Files related to synthetic homotopy theory.
+  Also contains `Homotopy/IdentitySystems` and `Homotopy/EncodeDecode`,
+  which give results for computing path types.
 
 - `Spectra/*`: Files related to spectra in the sense of stable
   homotopy theory.

contrib/HoTTBook.v

@@ -769,7 +769,10 @@ Definition Book_4_9_5 := @HoTT.Metatheory.FunextVarieties.WeakFunext_implies_Fun
 (* ================================================== thm:identity-systems *)
 (** Theorem 5.8.2 *)
 
-Definition Book_5_8_2_iv_implies_iii := @HoTT.PathAny.equiv_path_from_contr.
+Definition Book_5_8_2_i_implies_ii := @HoTT.Homotopy.IdentitySystems.homocontr_pfammap_identitysystem.
+Definition Book_5_8_2_ii_implies_iii := @HoTT.Homotopy.IdentitySystems.equiv_path_homocontr_pfammap.
+Definition Book_5_8_2_iii_implies_iv := @HoTT.Homotopy.IdentitySystems.contr_sigma_equiv_path.
+Definition Book_5_8_2_iv_implies_i := @HoTT.Homotopy.IdentitySystems.identitysystem_contr_sigma.
 
 (* ================================================== thm:ML-identity-systems *)
 (** Theorem 5.8.4 *)

contrib/SetoidRewrite.v

@@ -55,7 +55,7 @@ Defined.
          CRelationClasses.arrow) (GpdHom a).
 Proof.
   intros x y eq_xy eq_ax.
-  now transitivity x.
+  by transitivity x.
 Defined.
 
 (* forall a : A, x $== y -> a $== y -> a $== x *)

flake.nix

@@ -2,7 +2,7 @@
   description = "A Coq library for Homotopy Type Theory";
 
   inputs = {
-    nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";
+    nixpkgs.url = "github:NixOS/nixpkgs/master";
 
     flake-utils.url = "github:numtide/flake-utils";
   };
@@ -16,25 +16,36 @@
             coqPackages = pkgs.mkCoqPackages coq // {
               __attrsFailEvaluation = true;
             };
-          in { extraPackages ? [ coqPackages.coq-lsp ] }:
+          in
+          { extraPackages ? [ coqPackages.coq-lsp ] }:
           pkgs.mkShell {
-            buildInputs = with coqPackages;
+            buildInputs =
               [ pkgs.dune_3 pkgs.ocaml ] ++ extraPackages ++ [ coq ];
           };
-      in {
+      in
+      {
         packages.default = pkgs.coqPackages.mkCoqDerivation {
           pname = "hott";
-          version = "8.19";
+          version = "8.20";
           src = self;
           useDune = true;
         };
 
-        devShells.default = makeDevShell { coq = pkgs.coq_8_20; } { };
-        devShells.coq_8_19 = 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 =
-          makeDevShell { coq = pkgs.coq.override { version = "master"; }; } { };
+          makeDevShell
+            { coq = pkgs.coq.override { version = "master"; }; }
+            { extraPackages = [ ]; };
 
         formatter = pkgs.nixpkgs-fmt;
       });

theories/Algebra/AbGroups.v

@@ -10,6 +10,7 @@ Require Export HoTT.Algebra.AbGroups.Biproduct.
 Require Export HoTT.Algebra.AbGroups.AbHom.
 Require Export HoTT.Algebra.AbGroups.Cyclic.
 Require Export HoTT.Algebra.AbGroups.Centralizer.
+Require Export HoTT.Algebra.AbGroups.FiniteSum.
 
 (* The theory of Ext groups of abelian groups is in HoTT.Algebra.AbSES. *)
 

theories/Algebra/AbGroups/AbelianGroup.v

@@ -290,73 +290,3 @@ Proof.
   induction q.
   exact (p g).
 Defined.
-
-(** ** Finite Sums *)
-
-(** Indexed finite sum of abelian group elements. *)
-Definition ab_sum {A : AbGroup} (n : nat) (f : forall k, (k < n)%nat -> A) : A.
-Proof.
-  induction n as [|n IHn].
-  - exact zero.
-  - refine (f n _ + IHn _).
-    intros k 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. *)
-Definition ab_sum_const {A : AbGroup} (n : nat) (a : A)
-  (f : forall k, (k < n)%nat -> A) (p : forall k Hk, f k Hk = a)
-  : ab_sum n f = ab_mul n a.
-Proof.
-  induction n as [|n IHn] in f, p |- *.
-  - reflexivity.
-  - rhs_V nrapply (ap@{Set _} _ (int_nat_succ n)).
-    rhs nrapply grp_pow_succ.
-    simpl. f_ap.
-    apply IHn.
-    intros. apply p.
-Defined.
-
-(** If the function is zero in the range of a finite sum then the sum is zero. *)
-Definition ab_sum_zero {A : AbGroup} (n : nat)
-  (f : forall k, (k < n)%nat -> A) (p : forall k Hk, f k Hk = 0)
-  : ab_sum n f = 0.
-Proof.
-  lhs nrapply (ab_sum_const _ 0 f p).
-  apply grp_pow_unit.
-Defined.
-
-(** Finite sums distribute over addition. *)
-Definition ab_sum_plus {A : AbGroup} (n : nat) (f g : forall k, (k < n)%nat -> A)
-  : ab_sum n (fun k Hk => f k Hk + g k Hk)
-    = ab_sum n (fun k Hk => f k Hk) + ab_sum n (fun k Hk => g k Hk).
-Proof.
-  induction n as [|n IHn].
-  1: by rewrite grp_unit_l.
-  simpl.
-  rewrite <- !grp_assoc; f_ap.
-  rewrite IHn, ab_comm, <- grp_assoc; f_ap.
-  by rewrite ab_comm.
-Defined.
-
-(** Double finite sums commute. *)
-Definition ab_sum_sum {A : AbGroup} (m n : nat)
-  (f : forall i j, (i < m)%nat -> (j < n)%nat -> A)
-  : ab_sum m (fun i Hi => ab_sum n (fun j Hj => f i j Hi Hj))
-   = ab_sum n (fun j Hj => ab_sum m (fun i Hi => f i j Hi Hj)).
-Proof.
-  induction n as [|n IHn] in m, f |- *.
-  1: by nrapply ab_sum_zero.
-  lhs nrapply ab_sum_plus; cbn; f_ap.
-Defined.
-
-(** Finite sums are equal if the functions are equal in the range. *)
-Definition path_ab_sum {A : AbGroup} {n : nat} {f g : forall k, (k < n)%nat -> A}
-  (p : forall k Hk, f k Hk = g k Hk)
-  : ab_sum n f = ab_sum n g.
-Proof.
-  induction n as [|n IHn].
-  1: reflexivity.
-  cbn; f_ap.
-  by apply IHn.
-Defined.

theories/Algebra/AbGroups/Abelianization.v

@@ -150,15 +150,6 @@ Section Abel.
     exact a.
   Defined.
 
-  (** And its recursion version. *)
-  Definition Abel_rec_hprop (P : Type) `{IsHProp P}
-    (a : G -> P)
-    : Abel -> P.
-  Proof.
-    apply (Abel_rec _ a).
-    intros; apply path_ishprop.
-  Defined.
-
 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. *)
@@ -342,6 +333,14 @@ Proof.
   apply grp_homo_op.
 Defined.
 
+Definition abel_ind_homotopy {G H : Group} {f g : Hom (A:=Group) (abel G) H}
+  (p : f $o abel_unit $== g $o abel_unit)
+  : f $== g.
+Proof.
+  rapply Abel_ind_hprop.
+  rapply p.
+Defined.
+
 (** Finally we can prove that our construction abel is an abelianization. *)
 Global Instance isabelianization_abel {G : Group}
   : IsAbelianization (abel G) abel_unit.

theories/Algebra/AbGroups/FiniteSum.v

@@ -0,0 +1,78 @@
+Require Import Basics.Overture Basics.Tactics.
+Require Import Spaces.Nat.Core Spaces.Int.
+Require Export Classes.interfaces.canonical_names (Zero, zero, Plus).
+Require Export Classes.interfaces.abstract_algebra (IsAbGroup(..), abgroup_group, abgroup_commutative).
+Require Import AbelianGroup.
+
+Local Open Scope mc_scope.
+Local Open Scope mc_add_scope.
+
+(** * Finite Sums *)
+
+(** Indexed finite sum of abelian group elements. *)
+Definition ab_sum {A : AbGroup} (n : nat) (f : forall k, (k < n)%nat -> A) : A.
+Proof.
+  induction n as [|n IHn].
+  - exact zero.
+  - refine (f n _ + IHn _).
+    intros k 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. *)
+Definition ab_sum_const {A : AbGroup} (n : nat) (a : A)
+  (f : forall k, (k < n)%nat -> A) (p : forall k Hk, f k Hk = a)
+  : ab_sum n f = ab_mul n a.
+Proof.
+  induction n as [|n IHn] in f, p |- *.
+  - reflexivity.
+  - rhs_V nrapply (ap@{Set _} _ (int_nat_succ n)).
+    rhs nrapply grp_pow_succ.
+    simpl. f_ap.
+    apply IHn.
+    intros. apply p.
+Defined.
+
+(** If the function is zero in the range of a finite sum then the sum is zero. *)
+Definition ab_sum_zero {A : AbGroup} (n : nat)
+  (f : forall k, (k < n)%nat -> A) (p : forall k Hk, f k Hk = 0)
+  : ab_sum n f = 0.
+Proof.
+  lhs nrapply (ab_sum_const _ 0 f p).
+  apply grp_pow_unit.
+Defined.
+
+(** Finite sums distribute over addition. *)
+Definition ab_sum_plus {A : AbGroup} (n : nat) (f g : forall k, (k < n)%nat -> A)
+  : ab_sum n (fun k Hk => f k Hk + g k Hk)
+    = ab_sum n (fun k Hk => f k Hk) + ab_sum n (fun k Hk => g k Hk).
+Proof.
+  induction n as [|n IHn].
+  1: by rewrite grp_unit_l.
+  simpl.
+  rewrite <- !grp_assoc; f_ap.
+  rewrite IHn, ab_comm, <- grp_assoc; f_ap.
+  by rewrite ab_comm.
+Defined.
+
+(** Double finite sums commute. *)
+Definition ab_sum_sum {A : AbGroup} (m n : nat)
+  (f : forall i j, (i < m)%nat -> (j < n)%nat -> A)
+  : ab_sum m (fun i Hi => ab_sum n (fun j Hj => f i j Hi Hj))
+   = ab_sum n (fun j Hj => ab_sum m (fun i Hi => f i j Hi Hj)).
+Proof.
+  induction n as [|n IHn] in m, f |- *.
+  1: by nrapply ab_sum_zero.
+  lhs nrapply ab_sum_plus; cbn; f_ap.
+Defined.
+
+(** Finite sums are equal if the functions are equal in the range. *)
+Definition path_ab_sum {A : AbGroup} {n : nat} {f g : forall k, (k < n)%nat -> A}
+  (p : forall k Hk, f k Hk = g k Hk)
+  : ab_sum n f = ab_sum n g.
+Proof.
+  induction n as [|n IHn].
+  1: reflexivity.
+  cbn; f_ap.
+  by apply IHn.
+Defined.

theories/Algebra/AbGroups/FreeAbelianGroup.v

@@ -43,6 +43,16 @@ Definition FreeAbGroup_rec_beta_in {S : Type} {A : AbGroup} (f : S -> A)
   : FreeAbGroup_rec f o freeabgroup_in == f
   := fun _ => idpath.
 
+Definition FreeAbGroup_ind_homotopy {X : Type} {A : AbGroup}
+  {f f' : FreeAbGroup X $-> A}
+  (p : forall x, f (freeabgroup_in x) = f' (freeabgroup_in x))
+  : f $== f'.
+Proof.
+  snrapply abel_ind_homotopy.
+  snrapply FreeGroup_ind_homotopy.
+  snrapply p.
+Defined.
+
 (** The abelianization of a free group on a set is a free abelian group on that set. *)
 Global Instance isfreeabgroupon_isabelianization_isfreegroup `{Funext}
   {S : Type} {G : Group} {A : AbGroup} (f : S -> G) (g : G $-> A)

theories/Algebra/AbGroups/TensorProduct.v

@@ -1,7 +1,7 @@
 Require Import Basics.Overture Basics.Tactics.
 Require Import Types.Forall Types.Sigma Types.Prod.
 Require Import WildCat.Core WildCat.Equiv WildCat.Monoidal WildCat.Bifunctor.
-Require Import WildCat.NatTrans.
+Require Import WildCat.NatTrans WildCat.MonoidalTwistConstruction.
 Require Import Algebra.Groups.Group Algebra.Groups.QuotientGroup.
 Require Import Algebra.AbGroups.AbelianGroup Algebra.AbGroups.Biproduct.
 Require Import Algebra.AbGroups.AbHom Algebra.AbGroups.FreeAbelianGroup.

theories/Algebra/Categorical/MonoidObject.v

@@ -274,3 +274,43 @@ Section MonoidEnriched.
   Local Instance iscommutativemonoid_hom : IsCommutativeMonoid (x $-> y) := {}.
 
 End MonoidEnriched.
+
+(** ** Preservation of monoid objects by lax monoidal functors *)
+
+Definition mo_preserved {A B : Type}
+  {tensorA : A -> A -> A} {tensorB : B -> B -> B} {IA : A} {IB : B} 
+  (F : A -> B) `{IsMonoidalFunctor A B tensorA tensorB IA IB F} (x : A)
+  : IsMonoidObject tensorA IA x -> IsMonoidObject tensorB IB (F x).
+Proof.
+  intros mo_x.
+  snrapply Build_IsMonoidObject.
+  - exact (fmap F mo_mult $o fmap_tensor F (x, x)).
+  - exact (fmap F mo_unit $o fmap_unit).
+  - refine (((_ $@L (fmap10_comp tensorB _ _ _)) $@R _)
+      $@ _ $@ (_ $@L (fmap01_comp tensorB _ _ _)^$)).
+    refine (_ $@ (((_ $@L _^$) $@ cat_assoc_opp _ _ _) $@R _)
+      $@ cat_assoc _ _ _).
+    2: snrapply fmap_tensor_nat_r.
+    refine (_ $@ ((fmap2 _ mo_assoc $@ fmap_comp _ _ _) $@R _)
+      $@ cat_assoc_opp _ _ _ $@ (cat_assoc _ _ _ $@R _)).
+    refine (_ $@ ((fmap_comp _ _ _ $@ (fmap_comp _ _ _ $@R _))^$ $@R _)).
+    nrefine (cat_assoc _ _ _ $@ cat_assoc _ _ _ $@ (_ $@L _)
+      $@ cat_assoc_opp _ _ _ $@ cat_assoc_opp _ _ _).
+    refine (_ $@ (_ $@L (_^$ $@ cat_assoc _ _ _))).
+    2: snrapply fmap_tensor_assoc.
+    nrefine (cat_assoc_opp _ _ _ $@ (cat_assoc_opp _ _ _ $@R _)
+      $@ (((_ $@R _) $@ cat_assoc _ _ _) $@R _) $@ cat_assoc _ _ _).
+    snrapply fmap_tensor_nat_l.
+  - refine ((_ $@L fmap10_comp _ _ _ _) $@ cat_assoc _ _ _
+      $@ (_ $@L (cat_assoc_opp _ _ _ $@ (_ $@R _))) $@ _).
+    1: snrapply fmap_tensor_nat_l.
+    refine (cat_assoc_opp _ _ _ $@ ((cat_assoc_opp _ _ _ $@
+      (((fmap_comp _ _ _)^$ $@ fmap2 _ mo_left_unit) $@R _)) $@R _) $@ _^$).
+    snrapply fmap_tensor_left_unitor.
+  - refine ((_ $@L fmap01_comp _ _ _ _) $@ cat_assoc _ _ _
+      $@ (_ $@L (cat_assoc_opp _ _ _ $@ (_ $@R _))) $@ _).
+    1: snrapply fmap_tensor_nat_r.
+    refine (cat_assoc_opp _ _ _ $@ ((cat_assoc_opp _ _ _ $@
+      (((fmap_comp _ _ _)^$ $@ fmap2 _ mo_right_unit) $@R _)) $@R _) $@ _^$).
+    snrapply fmap_tensor_right_unitor.
+Defined.

theories/Algebra/Groups/Group.v

@@ -1,5 +1,5 @@
 Require Import Basics Types HProp HFiber HSet.
-Require Import PathAny.
+Require Import Homotopy.IdentitySystems.
 Require Import (notations) Classes.interfaces.canonical_names.
 Require Export (hints) Classes.interfaces.abstract_algebra.
 Require Export (hints) Classes.interfaces.canonical_names.