Adapt to coq/coq#18705 (#1850)

Adapt to coq/coq#18705 This is backward compatible (down to Coq 8.16). Co-authored-by: Niels van der Weide <nnmvdw@gmail.com>
UniMath · Feb 28, 2024 · a025e58 · a025e58
1 parent 0c15d08
commit a025e58
Show file tree

Hide file tree

Showing 109 changed files with 324 additions and 324 deletions.
diff --git a/UniMath/Algebra/GaussianElimination/Auxiliary.v b/UniMath/Algebra/GaussianElimination/Auxiliary.v
@@ -501,13 +501,13 @@ End Dual.
 
 Section Rings_and_Fields.
 
-  Coercion multlinvpair_of_multinvpair {R : rig} (x : R)
+  #[reversible] Coercion multlinvpair_of_multinvpair {R : rig} (x : R)
     : @multinvpair R x -> @multlinvpair R x.
   Proof.
     intros [y [xy yx]]. esplit; eauto.
   Defined.
 
-  Coercion multrinvpair_of_multinvpair {R : rig} (x : R)
+  #[reversible] Coercion multrinvpair_of_multinvpair {R : rig} (x : R)
     : @multinvpair R x -> @multrinvpair R x.
   Proof.
     intros [y [xy yx]]. esplit; eauto.

diff --git a/UniMath/Algebra/GaussianElimination/Matrices.v b/UniMath/Algebra/GaussianElimination/Matrices.v
@@ -356,14 +356,14 @@ Section Inverses.
       ((A ** B) = identity_matrix)
     × ((B ** A) = identity_matrix).
 
-  Coercion matrix_left_inverse_of_inverse {n : nat}
+  #[reversible] Coercion matrix_left_inverse_of_inverse {n : nat}
     (A : Matrix R n n)
     : @matrix_inverse n A -> @matrix_left_inverse n n A.
   Proof.
     intros [y [xy yx]]. esplit; eauto.
   Defined.
 
-  Coercion matrix_right_inverse_of_inverse {n : nat}
+  #[reversible] Coercion matrix_right_inverse_of_inverse {n : nat}
     (A : Matrix R n n)
     : @matrix_inverse n A -> @matrix_right_inverse n n A.
   Proof.

diff --git a/UniMath/Algebra/GroupAction.v b/UniMath/Algebra/GroupAction.v
@@ -142,7 +142,7 @@ Proof.
   apply setproperty.
 Defined.
 
-Coercion underlyingIso {G:gr} {X Y:Action G} (e:ActionIso X Y) : X ≃ Y := pr1 e.
+#[reversible] Coercion underlyingIso {G:gr} {X Y:Action G} (e:ActionIso X Y) : X ≃ Y := pr1 e.
 
 Lemma underlyingIso_incl {G:gr} {X Y:Action G} :
   isincl (underlyingIso : ActionIso X Y -> X ≃ Y).
@@ -282,7 +282,7 @@ Qed.
 
 Definition Torsor (G:gr) := total2 (@is_torsor G).
 
-Coercion underlyingAction {G} (X:Torsor G) := pr1 X : Action G.
+#[reversible] Coercion underlyingAction {G} (X:Torsor G) := pr1 X : Action G.
 
 Definition is_torsor_prop {G} (X:Torsor G) := pr2 X.
 

diff --git a/UniMath/Algebra/Universal/Signatures.v b/UniMath/Algebra/Universal/Signatures.v
@@ -52,12 +52,12 @@ Definition signature_simple : UU := ∑ (ns: nat), list (list (⟦ ns ⟧) ×
 Definition make_signature_simple {ns: nat} (ar: list (list (⟦ ns ⟧) × ⟦ ns ⟧))
   : signature_simple := ns ,, ar.
 
-Coercion signature_simple_compile (σ: signature_simple) : signature
+#[reversible] Coercion signature_simple_compile (σ: signature_simple) : signature
   := make_signature (⟦ pr1 σ ⟧ ,, isdeceqstn _) (stnset (length (pr2 σ))) (nth (pr2 σ)).
 
 Definition signature_simple_single_sorted : UU := list nat.
 
 Definition make_signature_simple_single_sorted (ar: list nat) : signature_simple_single_sorted := ar.
 
-Coercion signature_simple_single_sorted_compile (σ: signature_simple_single_sorted): signature
+#[reversible] Coercion signature_simple_single_sorted_compile (σ: signature_simple_single_sorted): signature
   := make_signature_single_sorted (stnset (length σ)) (nth σ).
diff --git a/UniMath/Algebra/Universal/Terms.v b/UniMath/Algebra/Universal/Terms.v
@@ -445,7 +445,7 @@ Section Term.
   Definition make_term {σ: signature} {s: sorts σ} {l: oplist σ} (lstack: isaterm s l)
     : term σ s := l ,, lstack.
 
-  Coercion term2oplist {σ: signature} {s: sorts σ}: term σ s → oplist σ := pr1.
+  #[reversible] Coercion term2oplist {σ: signature} {s: sorts σ}: term σ s → oplist σ := pr1.
 
   Definition term2proof {σ: signature} {s: sorts σ}: ∏ t: term σ s, isaterm s t := pr2.
 

diff --git a/UniMath/Algebra/Universal/VTerms.v b/UniMath/Algebra/Universal/VTerms.v
@@ -22,7 +22,7 @@ Section VTerms.
   Definition make_varspec (σ: signature) (varsupp: hSet) (varsorts: varsupp → sorts σ)
     : varspec σ := (varsupp,, varsorts).
 
-  Coercion varsupp {σ: signature}: varspec σ → hSet := pr1.
+  #[reversible] Coercion varsupp {σ: signature}: varspec σ → hSet := pr1.
 
   Definition varsort {σ: signature} {V: varspec σ}: V → sorts σ := pr2 V.
 

diff --git a/UniMath/AlgebraicTheories/AlgebraicTheories.v b/UniMath/AlgebraicTheories/AlgebraicTheories.v
@@ -57,7 +57,7 @@ Notation "f • g" :=
 
 Definition algebraic_theory : UU := algebraic_theory_cat.
 
-Coercion algebraic_theory_to_algebraic_theory_data (T : algebraic_theory)
+#[reversible] Coercion algebraic_theory_to_algebraic_theory_data (T : algebraic_theory)
   : algebraic_theory_data
   := pr1 T.
 

diff --git a/UniMath/AlgebraicTheories/AlgebraicTheoryMorphisms.v b/UniMath/AlgebraicTheories/AlgebraicTheoryMorphisms.v
@@ -43,7 +43,7 @@ Definition algebraic_theory_morphism
   : UU
   := algebraic_theory_cat⟦T, T'⟧.
 
-Coercion algebraic_theory_morphism_to_algebraic_theory_morphism_data
+#[reversible] Coercion algebraic_theory_morphism_to_algebraic_theory_morphism_data
   {T T' : algebraic_theory}
   (F : algebraic_theory_morphism T T')
   : algebraic_theory_morphism_data T T'

diff --git a/UniMath/AlgebraicTheories/Algebras.v b/UniMath/AlgebraicTheories/Algebras.v
@@ -38,7 +38,7 @@ Definition make_algebra_data
   : algebra_data T
   := A ,, action.
 
-Coercion algebra_data_to_hset
+#[reversible] Coercion algebra_data_to_hset
   {T : algebraic_theory}
   (A : algebra_data T)
   : hSet
@@ -80,7 +80,7 @@ Definition make_algebra
   : algebra T
   := pr1 A ,, pr2 A ,, H.
 
-Coercion algebra_to_algebra_data
+#[reversible] Coercion algebra_to_algebra_data
   {T : algebraic_theory}
   (A : algebra T)
   : algebra_data T

diff --git a/UniMath/AlgebraicTheories/FundamentalTheorem/CommonUtilities/MonoidActions.v b/UniMath/AlgebraicTheories/FundamentalTheorem/CommonUtilities/MonoidActions.v
@@ -104,7 +104,7 @@ End DataCat.
 
 Arguments action_ax /.
 
-Coercion monoid_action_data_to_hset {M : monoid} (x : monoid_action_data M) : hSet := pr1 x.
+#[reversible] Coercion monoid_action_data_to_hset {M : monoid} (x : monoid_action_data M) : hSet := pr1 x.
 
 Definition action
   {M : monoid}
@@ -169,7 +169,7 @@ Definition make_monoid_action
   : monoid_action M
   := X ,, H.
 
-Coercion monoid_action_to_monoid_action_data
+#[reversible] Coercion monoid_action_to_monoid_action_data
   (M : monoid)
   (f : monoid_action M)
   : monoid_action_data M

diff --git a/UniMath/AlgebraicTheories/LambdaCalculus.v b/UniMath/AlgebraicTheories/LambdaCalculus.v
@@ -320,7 +320,7 @@ Definition is_lambda_calculus (L : lambda_calculus_data) : UU :=
 
 Definition lambda_calculus : UU := ∑ L, is_lambda_calculus L.
 
-Coercion lambda_calculus_to_lambda_calculus_data (L : lambda_calculus)
+#[reversible] Coercion lambda_calculus_to_lambda_calculus_data (L : lambda_calculus)
   : lambda_calculus_data
   := pr1 L.
 

diff --git a/UniMath/AlgebraicTheories/LambdaTheories.v b/UniMath/AlgebraicTheories/LambdaTheories.v
@@ -39,7 +39,7 @@ Definition make_lambda_theory_data
   : lambda_theory_data
   := T ,, app ,, abs.
 
-Coercion lambda_theory_data_to_algebraic_theory (L : lambda_theory_data)
+#[reversible] Coercion lambda_theory_data_to_algebraic_theory (L : lambda_theory_data)
   : algebraic_theory
   := pr1 L.
 
@@ -62,7 +62,7 @@ Definition make_lambda_theory
   : lambda_theory
   := L ,, H.
 
-Coercion lambda_theory_to_lambda_theory_data (L : lambda_theory) : lambda_theory_data := pr1 L.
+#[reversible] Coercion lambda_theory_to_lambda_theory_data (L : lambda_theory) : lambda_theory_data := pr1 L.
 
 Definition app_comp
   (L : lambda_theory)

diff --git a/UniMath/AlgebraicTheories/LambdaTheoryMorphisms.v b/UniMath/AlgebraicTheories/LambdaTheoryMorphisms.v
@@ -48,7 +48,7 @@ Definition make_lambda_theory_morphism
   : lambda_theory_morphism L L'
   := (F ,, H) ,, tt.
 
-Coercion lambda_theory_morphism_to_algebraic_theory_morphism
+#[reversible] Coercion lambda_theory_morphism_to_algebraic_theory_morphism
   {L L' : lambda_theory}
   (F : lambda_theory_morphism L L')
   : algebraic_theory_morphism L L'

diff --git a/UniMath/AlgebraicTheories/Presheaves.v b/UniMath/AlgebraicTheories/Presheaves.v
@@ -68,7 +68,7 @@ Definition make_is_presheaf
 
 Definition presheaf (T : algebraic_theory) : UU := presheaf_cat T.
 
-Coercion presheaf_to_presheaf_data {T : algebraic_theory} (P : presheaf T)
+#[reversible] Coercion presheaf_to_presheaf_data {T : algebraic_theory} (P : presheaf T)
   : presheaf_data T
   := make_presheaf_data (pr1 P) (pr12 P).
 

diff --git a/UniMath/CategoryTheory/Actegories/Actegories.v b/UniMath/CategoryTheory/Actegories/Actegories.v
@@ -159,7 +159,7 @@ Definition actegory_actlaws {C : category} (Act : actegory C) : actegory_laws Ac
 Definition actegory_action_is_bifunctor {C : category} (Act : actegory C) : is_bifunctor Act
   := pr12 Act.
 
-Coercion actegory_action
+#[reversible] Coercion actegory_action
          {C : category}
          (Act : actegory C)
   : bifunctor V C C

diff --git a/UniMath/CategoryTheory/Additive.v b/UniMath/CategoryTheory/Additive.v
@@ -64,7 +64,7 @@ Section def_additive.
 
   Definition AdditiveCategory : UU := ∑ PA : PreAdditive, isAdditive PA.
 
-  Coercion Additive_to_PreAdditive (A : AdditiveCategory) : PreAdditive := pr1 A.
+  #[reversible] Coercion Additive_to_PreAdditive (A : AdditiveCategory) : PreAdditive := pr1 A.
 
   (** Accessor functions. *)
   Definition to_AdditiveStructure (A : CategoryWithAdditiveStructure) : AdditiveStructure A := pr2 A.

diff --git a/UniMath/CategoryTheory/Adjunctions/Core.v b/UniMath/CategoryTheory/Adjunctions/Core.v
@@ -119,7 +119,7 @@ Definition make_form_adjunction {A B : category} {F : functor A B} {G : functor
   Definition adjunction (A B : category) : UU
     := ∑ X : adjunction_data A B, form_adjunction' X.
 
-  Coercion data_from_adjunction {A B} (X : adjunction A B)
+  #[reversible] Coercion data_from_adjunction {A B} (X : adjunction A B)
     : adjunction_data _ _ := pr1 X.
 
   Definition make_adjunction {A B : category}
@@ -139,7 +139,7 @@ Definition make_form_adjunction {A B : category} {F : functor A B} {G : functor
              (adj : adjunction A B) : triangle_2_statement adj
     := pr2 (pr2 adj).
 
-  Coercion are_adjoints_from_adjunction {A B} (X : adjunction A B)
+  #[reversible] Coercion are_adjoints_from_adjunction {A B} (X : adjunction A B)
     : are_adjoints (left_functor X) (right_functor X).
   Proof.
     use make_are_adjoints.
@@ -159,7 +159,7 @@ Definition make_form_adjunction {A B : category} {F : functor A B} {G : functor
   Definition is_left_adjoint {A B : category} (F : functor A B) : UU :=
     ∑ (G : functor B A), are_adjoints F G.
 
-Coercion adjunction_data_from_is_left_adjoint {A B : category}
+  #[reversible] Coercion adjunction_data_from_is_left_adjoint {A B : category}
          {F : functor A B} (HF : is_left_adjoint F)
   : adjunction_data A B
   := (F,, _ ,,unit_from_are_adjoints (pr2 HF) ,,counit_from_are_adjoints (pr2 HF) ).

diff --git a/UniMath/CategoryTheory/Core/TwoCategories.v b/UniMath/CategoryTheory/Core/TwoCategories.v
@@ -43,7 +43,7 @@ Definition make_two_cat_data
   : two_cat_data
   := C ,, cellsC ,, id ,, vC ,, lW ,, rW.
 
-Coercion precategory_from_two_cat_data (C : two_cat_data)
+#[reversible] Coercion precategory_from_two_cat_data (C : two_cat_data)
   : precategory_data
   := pr1 C.
 
@@ -182,8 +182,8 @@ Definition make_two_precat
   : two_precat
   := C ,, HC.
 
-Coercion two_cat_category_from_two_cat (C : two_precat) : two_cat_category := pr1 C.
-Coercion two_cat_laws_from_two_cat (C : two_precat) : two_cat_laws C := pr2 C.
+#[reversible] Coercion two_cat_category_from_two_cat (C : two_precat) : two_cat_category := pr1 C.
+#[reversible] Coercion two_cat_laws_from_two_cat (C : two_precat) : two_cat_laws C := pr2 C.
 
 (* ----------------------------------------------------------------------------------- *)
 (** Laws projections.                                                                  *)
@@ -279,7 +279,7 @@ Definition make_two_cat
   : two_cat
   := C ,, HC.
 
-Coercion two_cat_to_two_precat
+#[reversible] Coercion two_cat_to_two_precat
          (C : two_cat)
   : two_precat
   := pr1 C.
@@ -354,7 +354,7 @@ Definition make_two_setcat
   : two_setcat
   := C ,, HC.
 
-Coercion two_setcat_to_two_cat
+#[reversible] Coercion two_setcat_to_two_cat
          (C : two_setcat)
   : two_cat
   := pr1 C.
@@ -376,7 +376,7 @@ Definition make_univalent_two_cat
   : univalent_two_cat
   := C ,, HC.
 
-Coercion univalent_two_cat_to_two_cat
+#[reversible] Coercion univalent_two_cat_to_two_cat
          (C : univalent_two_cat)
   : two_cat
   := pr1 C.

diff --git a/UniMath/CategoryTheory/Core/Univalence.v b/UniMath/CategoryTheory/Core/Univalence.v
@@ -68,9 +68,9 @@ Definition univalent_category : UU := ∑ C : category, is_univalent C.
 Definition make_univalent_category (C : category) (H : is_univalent C) : univalent_category
   := tpair _ C H.
 
-Coercion univalent_category_to_category (C : univalent_category) : category := pr1 C.
+#[reversible] Coercion univalent_category_to_category (C : univalent_category) : category := pr1 C.
 
-Coercion univalent_category_has_homsets (C : univalent_category)
+#[reversible] Coercion univalent_category_has_homsets (C : univalent_category)
   : has_homsets C
   := pr2 (pr1 C).
 

diff --git a/UniMath/CategoryTheory/DisplayedCats/Equivalences.v b/UniMath/CategoryTheory/DisplayedCats/Equivalences.v
@@ -95,7 +95,7 @@ Section DisplayedAdjunction.
     := ∑ AA : disp_adjunction_data A D D',
         triangle_1_statement_over AA × triangle_2_statement_over AA.
 
-  Coercion data_of_disp_adjunction (C C' : category) (A : adjunction C C')
+  #[reversible] Coercion data_of_disp_adjunction (C C' : category) (A : adjunction C C')
            D D' (AA : disp_adjunction A D D') : disp_adjunction_data _ _ _ := pr1 AA.
 
   Definition triangle_1_over {C C' : category}
@@ -208,12 +208,12 @@ Section DisplayedEquivalences.
     := ∑ AA : disp_adjunction E D D', @form_equiv_over _ _ E _  _ (pr1 AA).
   (* argument A is not inferred *)
 
-  Coercion adjunction_of_equiv_over {C C' : category} (E : adj_equiv C C')
+  #[reversible] Coercion adjunction_of_equiv_over {C C' : category} (E : adj_equiv C C')
            {D : disp_cat C} {D': disp_cat C'} (EE : equiv_over E D D')
     : disp_adjunction _ _ _ := pr1 EE.
 
 
-  Coercion axioms_of_equiv_over {C C' : category} (E : adj_equiv C C')
+  #[reversible] Coercion axioms_of_equiv_over {C C' : category} (E : adj_equiv C C')
            {D : disp_cat C} {D': disp_cat C'}
            (EE : equiv_over E D D') : form_equiv_over _
     := pr2 EE.

diff --git a/UniMath/CategoryTheory/DisplayedCats/Examples.v b/UniMath/CategoryTheory/DisplayedCats/Examples.v
@@ -81,8 +81,8 @@ Definition grp_inv_l {X : hSet} {G : grp_structure_data X}
 
 Definition grp_structure (X : hSet) : UU
   := ∑ G : grp_structure_data X, grp_structure_axioms G.
-Coercion grp_data {X} (G : grp_structure X) : grp_structure_data X := pr1 G.
-Coercion grp_axioms {X} (G : grp_structure X) : grp_structure_axioms _ := pr2 G.
+#[reversible] Coercion grp_data {X} (G : grp_structure X) : grp_structure_data X := pr1 G.
+#[reversible] Coercion grp_axioms {X} (G : grp_structure X) : grp_structure_axioms _ := pr2 G.
 
 Definition is_grp_hom {X Y : hSet} (f : X -> Y)
            (GX : grp_structure X) (GY : grp_structure Y) : UU

diff --git a/UniMath/CategoryTheory/DisplayedCats/Examples/AlgebraStructures.v b/UniMath/CategoryTheory/DisplayedCats/Examples/AlgebraStructures.v
@@ -61,7 +61,7 @@ Section MonadToStruct.
     : monad_algebra X
     := f ,, p.
 
-  Coercion monad_algebra_struct_to_mor
+  #[reversible] Coercion monad_algebra_struct_to_mor
            {X : hSet}
            (f : monad_algebra X)
     : M X --> X

diff --git a/UniMath/CategoryTheory/DisplayedCats/Examples/Arrow.v b/UniMath/CategoryTheory/DisplayedCats/Examples/Arrow.v
@@ -51,7 +51,7 @@ End Arrow_Disp.
 
 Definition arrow_dom {C : category} (f : arrow C) : C := pr11 f.
 Definition arrow_cod {C : category} (f : arrow C) : C := pr21 f.
-Coercion arrow_mor {C : category} (f : arrow C) := pr2 f.
+#[reversible] Coercion arrow_mor {C : category} (f : arrow C) := pr2 f.
 
 Definition arrow_mor00 {C : category} {f g : arrow C} (F : f --> g) := pr11 F.
 Definition arrow_mor11 {C : category} {f g : arrow C} (F : f --> g) := pr21 F.
@@ -67,7 +67,7 @@ Proof.
   apply pathsdirprod; assumption.
 Qed.
 
-Coercion mor_to_arrow_ob {C : category} {x y : C} (f : x --> y) : arrow C :=
+#[reversible] Coercion mor_to_arrow_ob {C : category} {x y : C} (f : x --> y) : arrow C :=
     (make_dirprod x y,, f).
 
 Definition mors_to_arrow_mor {C : category} {a b x y : C} (f : a --> b) (g : x --> y)

diff --git a/UniMath/CategoryTheory/DisplayedCats/Examples/MonadAlgebras.v b/UniMath/CategoryTheory/DisplayedCats/Examples/MonadAlgebras.v
@@ -32,11 +32,11 @@ Proof.
     exact (is_Algebra_mor T (X:=X') (Y:=Y') f).
 Defined.
 
-Coercion Algebra_from_MonadAlg_disp {C : category} {T : Monad C} {x : C}
+#[reversible] Coercion Algebra_from_MonadAlg_disp {C : category} {T : Monad C} {x : C}
     (X : MonadAlg_disp_ob_mor T x) : Algebra T :=
   (make_Algebra_data T x (pr1 X),, pr2 X).
 
-Coercion Algebra_mor_from_Algebra_mor_disp {C : category} {T : Monad C}
+#[reversible] Coercion Algebra_mor_from_Algebra_mor_disp {C : category} {T : Monad C}
     {x y : C} (X : MonadAlg_disp_ob_mor T x) (Y : MonadAlg_disp_ob_mor T y)
     {f : x --> y} (F : X -->[f] Y) : Algebra_mor T X Y := (f,, F).
 
@@ -130,11 +130,11 @@ Proof.
     exact (is_Coalgebra_mor T (X:=X') (Y:=Y') f).
 Defined.
 
-Coercion Coalgebra_from_ComonadCoalg_disp {C : category} {T : Comonad C} {x : C}
+#[reversible] Coercion Coalgebra_from_ComonadCoalg_disp {C : category} {T : Comonad C} {x : C}
     (X : ComonadCoalg_disp_ob_mor T x) : Coalgebra T :=
   (make_Coalgebra_data T x (pr1 X),, pr2 X).
 
-Coercion Coalgebra_mor_from_Coalgebra_mor_disp {C : category} {T : Comonad C}
+#[reversible] Coercion Coalgebra_mor_from_Coalgebra_mor_disp {C : category} {T : Comonad C}
     {x y : C} (X : ComonadCoalg_disp_ob_mor T x) (Y : ComonadCoalg_disp_ob_mor T y)
     {f : x --> y} (F : X -->[f] Y) : Coalgebra_mor T X Y := (f,, F).