Merge pull request #1763 from jdchristensen/8.18-fixes

Adjustments to support Coq 8.18.0
HoTT · Sep 18, 2023 · 4e9183a · 4e9183a
2 parents 6f143f9 + 7bb620c
commit 4e9183a
Show file tree

Hide file tree

Showing 6 changed files with 54 additions and 56 deletions.
diff --git a/theories/Basics/Equivalences.v b/theories/Basics/Equivalences.v
@@ -93,7 +93,7 @@ Section IsEquivHomotopic.
   Let sect := (fun a:A => (ap f^-1 (h a))^ @ eissect f a).
 
   (* We prove the triangle identity with rewrite tactics.  Since we lose control over the proof term that way, we make the result opaque with "Qed". *)
-  Let adj (a : A) : retr (g a) = ap g (sect a).
+  Local Definition adj (a : A) : retr (g a) = ap g (sect a).
   Proof.
     unfold sect, retr.
     rewrite ap_pp. apply moveR_Vp.

diff --git a/theories/Categories/LaxComma/Core.v b/theories/Categories/LaxComma/Core.v
@@ -175,7 +175,7 @@ Module Export LaxCommaCoreNotations.
   (** We play some games to get nice notations for lax comma categories. *)
   Section tc_notation_boiler_plate.
     Local Open Scope type_scope.
-    Class LCC_Builder {A B C} (x : A) (y : B) (z : C) := lcc_builder_dummy : True.
+    Class LCC_Builder {A B C} (x : A) (y : B) (z : C) : Set := lcc_builder_dummy : True.
     Definition get_LCC `{@LCC_Builder A B C x y z} : C := z.
 
     Global Arguments get_LCC / {A B C} x y {z} {_}.
@@ -210,7 +210,7 @@ Module Export LaxCommaCoreNotations.
     : LCC_Builder (@sub_pre_cat _ P HF) a (@lax_coslice_category_over _ P HF a _) | 10
       := I.
 
-    Class OLCC_Builder {A B C} (x : A) (y : B) (z : C) := olcc_builder_dummy : True.
+    Class OLCC_Builder {A B C} (x : A) (y : B) (z : C) : Set := olcc_builder_dummy : True.
 
     Definition get_OLCC `{@OLCC_Builder A B C x y z} : C := z.
 

diff --git a/theories/Classes/implementations/binary_naturals.v b/theories/Classes/implementations/binary_naturals.v
@@ -62,15 +62,15 @@ Section binary_equiv.
     | double2 n' => Double2 (unary' n')
     end.
 
-  Let succunary (n : binnat) : unary' (Succ n) = S (unary' n).
+  Local Definition succunary (n : binnat) : unary' (Succ n) = S (unary' n).
   Proof.
     induction n.
     - reflexivity.
     - reflexivity.
     - simpl. rewrite IHn. reflexivity.
   Qed.
 
-  Let unarybinary : unary' o binary == idmap.
+  Local Definition unarybinary : unary' o binary == idmap.
   Proof.
     intros n; induction n as [|n IHn].
     - reflexivity.
@@ -93,7 +93,7 @@ Section binary_equiv.
       rewrite IHn. reflexivity.
   Qed.
 
-  Let binaryunary : binary o unary' == idmap.
+  Local Definition binaryunary : binary o unary' == idmap.
   Proof.
     intros n; induction n.
     - reflexivity.
@@ -421,24 +421,15 @@ Section naturals.
           reflexivity.
     Qed.
 
-    Let f_preserves_0: toR 0 =  0.
-    Proof. reflexivity. Qed.
-
-    Let f_preserves_1: toR 1 = 1.
-    Proof.
-      rewrite (f_nat 1).
-      reflexivity.
-    Qed.
-
-    Let f_preserves_plus (a a' : binnat) : toR (a + a') = toR a + toR a'.
+    Local Definition f_preserves_plus (a a' : binnat) : toR (a + a') = toR a + toR a'.
     Proof.
       rewrite f_nat, f_nat, f_nat.
       unfold Compose.
       rewrite <- (unaryplus a a').
       apply nat_to_sr_morphism.
     Qed.
 
-    Let f_preserves_mult (a a' : binnat) : toR (a * a') = toR a * toR a'.
+    Local Definition f_preserves_mult (a a' : binnat) : toR (a * a') = toR a * toR a'.
     Proof.
       rewrite f_nat, f_nat, f_nat.
       unfold Compose.
@@ -449,8 +440,13 @@ Section naturals.
     Global Instance binnat_to_sr_morphism
       : IsSemiRingPreserving toR.
     Proof.
-      repeat (split;try apply _);trivial.
-    Qed.
+      split; split.
+      - rapply f_preserves_plus.
+      - reflexivity.
+      - rapply f_preserves_mult.
+      - unfold IsUnitPreserving.
+        apply f_nat.
+    Defined.
 
     Lemma binnat_toR_unique (h : binnat -> R) `{!IsSemiRingPreserving h} : forall x,
         toR x = h x.
@@ -475,7 +471,7 @@ End naturals.
 
 Section decidable.
 
-  Let ineq_bzero_double1 n : bzero <> double1 n.
+  Local Definition ineq_bzero_double1 n : bzero <> double1 n.
   Proof.
     intros p.
     change ((fun x => match x with | double1 y => Unit | _ => Empty end) bzero).
@@ -484,7 +480,7 @@ Section decidable.
     - exact tt.
   Qed.
 
-  Let ineq_bzero_double2 n : bzero <> double2 n.
+  Local Definition ineq_bzero_double2 n : bzero <> double2 n.
   Proof.
     intros p.
     change ((fun x => match x with | double2 y => Unit | _ => Empty end) bzero).
@@ -493,7 +489,7 @@ Section decidable.
     - exact tt.
   Qed.
 
-  Let ineq_double1_double2 m n : double1 m <> double2 n.
+  Local Definition ineq_double1_double2 m n : double1 m <> double2 n.
   Proof.
     intros p.
     change ((fun x => match x with | double2 y => Unit | _ => Empty end) (double1 m)).
@@ -502,7 +498,7 @@ Section decidable.
     - exact tt.
   Qed.
 
-  Let undouble (m : binnat) : binnat :=
+  Local Definition undouble (m : binnat) : binnat :=
     match m with
     | bzero => bzero
     | double1 k => k
@@ -602,7 +598,7 @@ Section minus.
     | double2 m' => double1 m'
     end.
 
-  Let succ_double (m : binnat) : Succ (double m) = double1 m.
+  Local Definition succ_double (m : binnat) : Succ (double m) = double1 m.
   Proof.
     induction m.
     - reflexivity.
@@ -612,7 +608,7 @@ Section minus.
       rewrite IHm; reflexivity.
   Qed.
 
-  Let double_succ (m : binnat) : double (Succ m) = double2 m.
+  Local Definition double_succ (m : binnat) : double (Succ m) = double2 m.
   Proof.
     induction m.
     - reflexivity.
@@ -622,24 +618,24 @@ Section minus.
       rewrite IHm; reflexivity.
   Qed.
 
-  Let pred_succ (m : binnat) : Pred (Succ m) = m.
+  Local Definition pred_succ (m : binnat) : Pred (Succ m) = m.
   Proof.
     induction m; try reflexivity.
     - exact (double_succ m).
   Qed.
 
-  Let double_pred (m : binnat) : double (Pred m) = Pred (Pred (double m)).
+  Local Definition double_pred (m : binnat) : double (Pred m) = Pred (Pred (double m)).
   Proof.
     induction m; try reflexivity.
     - exact (double_succ (double m))^.
   Qed.
 
-  Let pred_double2 (m : binnat) : Pred (double2 m) = double1 m.
+  Local Definition pred_double2 (m : binnat) : Pred (double2 m) = double1 m.
   Proof.
     induction m; reflexivity.
   Qed.
 
-  Let pred_double1 (m : binnat) : Pred (double1 m) = double m.
+  Local Definition pred_double1 (m : binnat) : Pred (double1 m) = double m.
   Proof.
     induction m; reflexivity.
   Qed.
@@ -662,17 +658,17 @@ Section minus.
 
   Global Instance binnat_cut_minus: CutMinus binnat := binnat_cut_minus'.
 
-  Let binnat_minus_zero (m : binnat) : m ∸ bzero = m.
+  Local Definition binnat_minus_zero (m : binnat) : m ∸ bzero = m.
   Proof.
     induction m; reflexivity.
   Qed.
 
-  Let binnat_zero_minus (m : binnat) : bzero ∸ m = bzero.
+  Local Definition binnat_zero_minus (m : binnat) : bzero ∸ m = bzero.
   Proof.
     induction m; reflexivity.
   Qed.
 
-  Let pred_succ_minus (m n : binnat) : Pred (Succ m ∸ n) = m ∸ n.
+  Local Definition pred_succ_minus (m n : binnat) : Pred (Succ m ∸ n) = m ∸ n.
   Proof.
     revert n; induction m; intros n; induction n; try reflexivity.
     - change (Pred (double (bzero ∸ n)) = bzero).
@@ -692,15 +688,15 @@ Section minus.
       exact (IHm n).
   Qed.
 
-  Let double_cases (m : binnat) : (bzero = double m) + hfiber double2 (double m).
+  Local Definition double_cases (m : binnat) : (bzero = double m) + hfiber double2 (double m).
   Proof.
     induction m.
     - left; reflexivity.
     - right; exists (double m); reflexivity.
     - right; exists (Succ (double m)); reflexivity.
   Defined.
 
-  Let binnat_minus_succ (m n : binnat) : Succ m ∸ Succ n = m ∸ n.
+  Local Definition binnat_minus_succ (m n : binnat) : Succ m ∸ Succ n = m ∸ n.
   Proof.
     revert n; induction m; intros n; induction n; try reflexivity.
     - change (Pred (double (bzero ∸ n)) = bzero ∸ double1 n).
@@ -719,7 +715,7 @@ Section minus.
       rewrite IHm. reflexivity.
   Qed.
 
-  Let binaryminus (x y : nat) : binary x ∸ binary y = binary (x ∸ y).
+  Local Definition binaryminus (x y : nat) : binary x ∸ binary y = binary (x ∸ y).
   Proof.
     revert y; induction x; intros y; induction y; try reflexivity.
     - apply binnat_zero_minus.
@@ -728,7 +724,7 @@ Section minus.
       rewrite IHx. reflexivity.
   Qed.
 
-  Let unaryminus (m n : binnat) : unary m ∸ unary n = unary (m ∸ n).
+  Local Definition unaryminus (m n : binnat) : unary m ∸ unary n = unary (m ∸ n).
   Proof.
     etransitivity (unary (binary (_^-1 m ∸ _^-1 n))).
     - apply ((eissect binary (unary m ∸ unary n)) ^).

diff --git a/theories/Classes/implementations/peano_naturals.v b/theories/Classes/implementations/peano_naturals.v
@@ -18,8 +18,11 @@ Universe N.
 
 Let natpaths := @paths@{N} nat.
 Infix "=N=" := natpaths.
-Let natpaths_symm : Symmetric@{N N} natpaths.
-Proof. unfold natpaths;apply _. Qed.
+
+Definition natpaths_symm : Symmetric@{N N} natpaths.
+Proof.
+  unfold natpaths; apply _.
+Defined.
 
 Global Instance nat_0: Zero@{N} nat := 0%nat.
 Global Instance nat_1: One@{N} nat := 1%nat.
@@ -582,20 +585,14 @@ Section for_another_semiring.
 
 (*   Add Ring R: (rings.stdlib_semiring_theory R). *)
 
-  Let f_preserves_0: toR 0 =  0.
-  Proof. reflexivity. Qed.
-
-  Let f_preserves_1: toR 1 = 1.
-  Proof. reflexivity. Qed.
-
-  Let f_S : forall x, toR (S x) = 1 + toR x.
+  Local Definition f_S : forall x, toR (S x) = 1 + toR x.
   Proof.
   intros [|x].
   - symmetry;apply plus_0_r.
   - reflexivity.
-  Qed.
+  Defined.
 
-  Let f_preserves_plus a a': toR (a + a') = toR a + toR a'.
+  Local Definition f_preserves_plus a a': toR (a + a') = toR a + toR a'.
   Proof.
   induction a as [|a IHa].
   - change (toR a' = 0 + toR a').
@@ -605,7 +602,7 @@ Section for_another_semiring.
     apply associativity.
   Qed.
 
-  Let f_preserves_mult a a': toR (a * a') = toR a * toR a'.
+  Local Definition f_preserves_mult a a': toR (a * a') = toR a * toR a'.
   Proof.
   induction a as [|a IHa].
   - change (0 = 0 * toR a').
@@ -620,7 +617,11 @@ Section for_another_semiring.
   Global Instance nat_to_sr_morphism
     : IsSemiRingPreserving (naturals_to_semiring nat R).
   Proof.
-  repeat (split;try apply _);trivial.
+    split; split.
+    - rapply f_preserves_plus.
+    - reflexivity.
+    - rapply f_preserves_mult.
+    - reflexivity.
   Defined.
 
   Lemma toR_unique (h : nat -> R) `{!IsSemiRingPreserving h} x :

diff --git a/theories/Colimits/Pushout.v b/theories/Colimits/Pushout.v
@@ -61,8 +61,8 @@ End PushoutInd.
 Arguments Pushout : simpl never.
 Arguments push : simpl never.
 Arguments pglue : simpl never.
-Arguments Pushout_ind : simpl never.
 Arguments Pushout_ind_beta_pglue : simpl never.
+(** However, we do allow [Pushout_ind] to simplify, as it computes on point constructors. *)
 
 Definition Pushout_rec {A B C} {f : A -> B} {g : A -> C} (P : Type)
   (pushb : B -> P)
@@ -259,7 +259,7 @@ Section EquivSigmaPushout.
           (A : X -> Type) (B : X -> Type) (C : X -> Type)
           (f : forall x, A x -> B x) (g : forall x, A x -> C x).
 
-  Let esp1 : { x : X & Pushout (f x) (g x) }
+  Local Definition esp1 : { x : X & Pushout (f x) (g x) }
              -> Pushout (functor_sigma idmap f) (functor_sigma idmap g).
   Proof.
     intros [x p].
@@ -269,7 +269,7 @@ Section EquivSigmaPushout.
     + intros a; cbn. exact (pglue (x;a)).
   Defined.
 
-  Let esp1_beta_pglue (x : X) (a : A x)
+  Local Definition esp1_beta_pglue (x : X) (a : A x)
     : ap esp1 (path_sigma' (fun x => Pushout (f x) (g x)) 1 (pglue a))
       = pglue (x;a).
   Proof.
@@ -280,7 +280,7 @@ Section EquivSigmaPushout.
     reflexivity.
   Qed.
 
-  Let esp2 : Pushout (functor_sigma idmap f) (functor_sigma idmap g)
+  Local Definition esp2 : Pushout (functor_sigma idmap f) (functor_sigma idmap g)
              -> { x : X & Pushout (f x) (g x) }.
   Proof.
     srefine (Pushout_rec _ _ _ _).
@@ -291,7 +291,7 @@ Section EquivSigmaPushout.
       apply pglue.
   Defined.
 
-  Let esp2_beta_pglue (x : X) (a : A x)
+  Local Definition esp2_beta_pglue (x : X) (a : A x)
     : ap esp2 (pglue (x;a)) = path_sigma' (fun x:X => Pushout (f x) (g x)) 1 (pglue a).
   Proof.
     unfold esp2.

diff --git a/theories/Modalities/ReflectiveSubuniverse.v b/theories/Modalities/ReflectiveSubuniverse.v
@@ -1550,7 +1550,8 @@ Global Existing Instance isconnected_hfiber_conn_map.
 
 Section ConnectedMaps.
   Context `{Univalence} `{Funext}.
-  Context (O : ReflectiveSubuniverse).
+  Universe i.
+  Context (O : ReflectiveSubuniverse@{i}).
 
   (** Any equivalence is connected *)
   Global Instance conn_map_isequiv {A B : Type} (f : A -> B) `{IsEquiv _ _ f}
@@ -1564,7 +1565,7 @@ Section ConnectedMaps.
   : IsConnMap O f -> IsConnMap O g.
   Proof.
     intros ? b.
-    exact (isconnected_equiv O (hfiber f b)
+    exact (isconnected_equiv O (hfiber@{i i} f b)
                              (equiv_hfiber_homotopic f g h b) _).
   Defined.