From a025e583854a0bee42b790d283ea1bed698c5341 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 28 Feb 2024 12:49:06 +0100 Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/18705 (#1850) Adapt to https://github.com/coq/coq/pull/18705 This is backward compatible (down to Coq 8.16). Co-authored-by: Niels van der Weide --- .../Algebra/GaussianElimination/Auxiliary.v | 4 +- .../Algebra/GaussianElimination/Matrices.v | 4 +- UniMath/Algebra/GroupAction.v | 4 +- UniMath/Algebra/Universal/Signatures.v | 4 +- UniMath/Algebra/Universal/Terms.v | 2 +- UniMath/Algebra/Universal/VTerms.v | 2 +- UniMath/AlgebraicTheories/AlgebraicTheories.v | 2 +- .../AlgebraicTheoryMorphisms.v | 2 +- UniMath/AlgebraicTheories/Algebras.v | 4 +- .../CommonUtilities/MonoidActions.v | 4 +- UniMath/AlgebraicTheories/LambdaCalculus.v | 2 +- UniMath/AlgebraicTheories/LambdaTheories.v | 4 +- .../AlgebraicTheories/LambdaTheoryMorphisms.v | 2 +- UniMath/AlgebraicTheories/Presheaves.v | 2 +- .../CategoryTheory/Actegories/Actegories.v | 2 +- UniMath/CategoryTheory/Additive.v | 2 +- UniMath/CategoryTheory/Adjunctions/Core.v | 6 +- UniMath/CategoryTheory/Core/TwoCategories.v | 12 +- UniMath/CategoryTheory/Core/Univalence.v | 4 +- .../DisplayedCats/Equivalences.v | 6 +- .../CategoryTheory/DisplayedCats/Examples.v | 4 +- .../Examples/AlgebraStructures.v | 2 +- .../DisplayedCats/Examples/Arrow.v | 4 +- .../DisplayedCats/Examples/MonadAlgebras.v | 8 +- .../CategoryTheory/DisplayedCats/Fibrations.v | 6 +- .../Structures/CartesianStructure.v | 8 +- .../Structures/StructureLimitsAndColimits.v | 12 +- .../Structures/StructuresSmashProduct.v | 6 +- .../Colimits/EnrichedBinaryCoproducts.v | 8 +- .../Colimits/EnrichedCoequalizers.v | 8 +- .../EnrichedCats/Colimits/EnrichedColimits.v | 4 +- .../Colimits/EnrichedConicalColimits.v | 6 +- .../EnrichedCats/Colimits/EnrichedCopowers.v | 4 +- .../Colimits/EnrichedCoproducts.v | 8 +- .../EnrichedCats/Colimits/EnrichedInitial.v | 6 +- .../CategoryTheory/EnrichedCats/Enrichment.v | 6 +- .../EnrichedCats/EnrichmentAdjunction.v | 4 +- .../EnrichedCats/EnrichmentFunctor.v | 2 +- .../EnrichedCats/EnrichmentMonad.v | 4 +- .../Limits/EnrichedBinaryProducts.v | 8 +- .../Limits/EnrichedConicalLimits.v | 6 +- .../EnrichedCats/Limits/EnrichedEqualizers.v | 8 +- .../EnrichedCats/Limits/EnrichedLimits.v | 4 +- .../EnrichedCats/Limits/EnrichedPowers.v | 4 +- .../EnrichedCats/Limits/EnrichedProducts.v | 8 +- .../EnrichedCats/Limits/EnrichedTerminal.v | 6 +- .../Equivalences/CompositesAndInverses.v | 2 +- UniMath/CategoryTheory/Equivalences/Core.v | 10 +- .../ExactCategories/ExactCategories.v | 22 ++-- UniMath/CategoryTheory/FunctorAlgebras.v | 2 +- UniMath/CategoryTheory/FunctorCoalgebras.v | 2 +- .../IndexedCategories/IndexedCategory.v | 2 +- .../IndexedCategories/IndexedFunctor.v | 2 +- UniMath/CategoryTheory/Limits/Coends.v | 8 +- UniMath/CategoryTheory/Limits/Ends.v | 8 +- .../CategoryTheory/Monads/ComonadCoalgebras.v | 6 +- UniMath/CategoryTheory/Monads/Comonads.v | 6 +- UniMath/CategoryTheory/Monads/KTriples.v | 4 +- UniMath/CategoryTheory/Monads/Kleisli.v | 2 +- UniMath/CategoryTheory/Monads/LModules.v | 6 +- UniMath/CategoryTheory/Monads/MonadAlgebras.v | 6 +- UniMath/CategoryTheory/Monads/Monads.v | 6 +- .../CategoryTheory/Monads/RelativeModules.v | 10 +- .../CategoryTheory/Monads/RelativeMonads.v | 8 +- UniMath/CategoryTheory/Monoidal/Adjunctions.v | 4 +- .../CategoriesOfMonoids.v | 2 +- .../DisplayedMonoidalTensored.v | 2 +- UniMath/CategoryTheory/Monoidal/Categories.v | 6 +- .../Monoidal/FunctorCategories.v | 2 +- UniMath/CategoryTheory/Monoidal/Functors.v | 12 +- UniMath/CategoryTheory/Monoidal/StrongMonad.v | 2 +- .../Monoidal/Structure/Cartesian.v | 4 +- .../Monoidal/Structure/Closed.v | 2 +- .../Monoidal/Structure/Symmetric.v | 4 +- UniMath/CategoryTheory/PointedFunctors.v | 4 +- UniMath/CategoryTheory/Profunctors/Squares.v | 4 +- .../Profunctors/Transformation.v | 4 +- UniMath/CategoryTheory/Retracts.v | 4 +- .../SkewMonoidal/CategoriesOfMonoids.v | 6 +- .../SkewMonoidal/SkewMonoidalCategories.v | 4 +- .../TwoSidedDisplayedCats/DisplayedFunctor.v | 2 +- .../TwoSidedDisplayedCats/Examples/Lenses.v | 2 +- .../TwoSidedDisplayedCats/Isos.v | 4 +- .../TwoSidedDisplayedCats/Strictness.v | 2 +- .../TwoSidedDisplayedCats/TwoSidedDispCat.v | 4 +- .../TwoSidedDisplayedCats/Univalence.v | 2 +- UniMath/CategoryTheory/rezk_completion.v | 2 +- UniMath/Combinatorics/MetricTree.v | 2 +- UniMath/Induction/FunctorAlgebras_legacy.v | 2 +- UniMath/Induction/W/Wtypes.v | 12 +- .../Generated/GenericFreeMonoid.v | 122 +++++++++--------- .../Generated/GenericFreeMonoidSequence.v | 2 +- .../Generated/LiftingWithClass.v | 4 +- UniMath/ModelCategories/NWFS.v | 2 +- .../FixedPointTheorems.v | 20 +-- UniMath/OrderTheory/DCPOs/Basis/Basis.v | 6 +- .../OrderTheory/DCPOs/Basis/CompactBasis.v | 4 +- UniMath/OrderTheory/DCPOs/Core/Basics.v | 14 +- UniMath/OrderTheory/DCPOs/Core/DirectedSets.v | 2 +- .../OrderTheory/DCPOs/Core/ScottContinuous.v | 6 +- .../OrderTheory/DCPOs/Core/ScottTopology.v | 4 +- UniMath/OrderTheory/DCPOs/Elements/Maximal.v | 2 +- .../DCPOs/Examples/IdealCompletion.v | 4 +- .../DCPOs/FixpointTheorems/Pataraia.v | 2 +- UniMath/OrderTheory/Posets/PointedPosets.v | 4 +- .../EnrichedEffectCalculus/EECModel.v | 2 +- .../Semantics/LinearLogic/LafontCategory.v | 2 +- .../Semantics/LinearLogic/LinearCategory.v | 4 +- .../Semantics/LinearLogic/LinearNonLinear.v | 2 +- 109 files changed, 324 insertions(+), 324 deletions(-) diff --git a/UniMath/Algebra/GaussianElimination/Auxiliary.v b/UniMath/Algebra/GaussianElimination/Auxiliary.v index e262cdc92f..09aa87f7f7 100644 --- 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 index 082471259b..26bcc8090c 100644 --- 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 index 55e03fe257..3f159a125f 100644 --- 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 index 67606886fd..a4864c96da 100644 --- 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 index 78b9952587..1d3d135873 100644 --- 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 index 485d80e1be..cb06e1c063 100644 --- 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 index 5ca0a7938d..c322e728c1 100644 --- 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 index 4b170abacd..8facc295b9 100644 --- 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 index 1534e7d119..608daa82cc 100644 --- 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 index 1eecfe899d..8519d35b9f 100644 --- 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 index a50ba73c28..40872e7848 100644 --- 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 index 3262c1018d..3fdf70549b 100644 --- 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 index cc49162756..b2ff095085 100644 --- 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 index 04ff3c7a7d..1b709defda 100644 --- 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 index b40bc8354c..184758095d 100644 --- 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 index 08584d60c0..da6d29d82a 100644 --- 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 index 2d65d737db..aa81219d39 100644 --- 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 index f21b341881..127fe27217 100644 --- 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 index bc8713a6ef..eb742f4fa5 100644 --- 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 index d3b12adb63..2cd6c128b4 100644 --- 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 index 71d091e1c0..b6d7518384 100644 --- 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 index a28337e7ed..8acc241eaf 100644 --- 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 index 1d96d51ad6..890adf7f54 100644 --- 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 index 54401a878e..329b1c0044 100644 --- 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). diff --git a/UniMath/CategoryTheory/DisplayedCats/Fibrations.v b/UniMath/CategoryTheory/DisplayedCats/Fibrations.v index b720a229c5..aac6b7fd9a 100644 --- a/UniMath/CategoryTheory/DisplayedCats/Fibrations.v +++ b/UniMath/CategoryTheory/DisplayedCats/Fibrations.v @@ -243,7 +243,7 @@ Definition cartesian_disp_functor : UU := ∑ (FF : disp_functor F D₁ D₂), is_cartesian_disp_functor FF. -Coercion disp_functor_of_cartesian_disp_functor +#[reversible] Coercion disp_functor_of_cartesian_disp_functor {C₁ C₂ : category} {F : C₁ ⟶ C₂} {D₁ : disp_cat C₁} @@ -502,7 +502,7 @@ Definition is_discrete_fibration {C : category} (D : disp_cat C) : UU Definition discrete_fibration C : UU := ∑ D : disp_cat C, is_discrete_fibration D. -Coercion disp_cat_from_discrete_fibration C (D : discrete_fibration C) +#[reversible] Coercion disp_cat_from_discrete_fibration C (D : discrete_fibration C) : disp_cat C := pr1 D. Definition unique_lift {C} {D : discrete_fibration C} {c c'} (f : c' --> c) (d : D c) @@ -1229,7 +1229,7 @@ Definition opcartesian_disp_functor : UU := ∑ (FF : disp_functor F D₁ D₂), is_opcartesian_disp_functor FF. -Coercion disp_functor_of_opcartesian_disp_functor +#[reversible] Coercion disp_functor_of_opcartesian_disp_functor {C₁ C₂ : category} {F : C₁ ⟶ C₂} {D₁ : disp_cat C₁} diff --git a/UniMath/CategoryTheory/DisplayedCats/Structures/CartesianStructure.v b/UniMath/CategoryTheory/DisplayedCats/Structures/CartesianStructure.v index c1dde61b27..e0c39c7f7a 100644 --- a/UniMath/CategoryTheory/DisplayedCats/Structures/CartesianStructure.v +++ b/UniMath/CategoryTheory/DisplayedCats/Structures/CartesianStructure.v @@ -119,7 +119,7 @@ Definition hset_struct : UU := ∑ (P : hset_struct_data), hset_struct_laws P. -Coercion hset_struct_to_data +#[reversible] Coercion hset_struct_to_data (P : hset_struct) : hset_struct_data := pr1 P. @@ -366,7 +366,7 @@ Definition hset_cartesian_struct_data (PY : P Y), P (X × Y)%set). -Coercion hset_cartesian_struct_datat_to_struct +#[reversible] Coercion hset_cartesian_struct_datat_to_struct (P : hset_cartesian_struct_data) : hset_struct := pr1 P. @@ -426,7 +426,7 @@ Definition hset_cartesian_struct : UU := ∑ (P : hset_cartesian_struct_data), hset_cartesian_struct_laws P. -Coercion hset_cartesian_struct_to_data +#[reversible] Coercion hset_cartesian_struct_to_data (P : hset_cartesian_struct) : hset_cartesian_struct_data := pr1 P. @@ -737,7 +737,7 @@ Definition discrete_hset_struct := ∑ (PX : discrete_hset_struct_data P), discrete_hset_struct_laws PX. -Coercion discrete_hset_struct_to_data +#[reversible] Coercion discrete_hset_struct_to_data {P : hset_struct} (PX : discrete_hset_struct P) : discrete_hset_struct_data P diff --git a/UniMath/CategoryTheory/DisplayedCats/Structures/StructureLimitsAndColimits.v b/UniMath/CategoryTheory/DisplayedCats/Structures/StructureLimitsAndColimits.v index 3927e01a4d..20b145f2bd 100644 --- a/UniMath/CategoryTheory/DisplayedCats/Structures/StructureLimitsAndColimits.v +++ b/UniMath/CategoryTheory/DisplayedCats/Structures/StructureLimitsAndColimits.v @@ -106,7 +106,7 @@ Definition hset_cartesian_closed_struct_data (constP : struct_contains_constant P), closed_under_fun_data P. -Coercion hset_cartesian_closed_struct_data_to_struct +#[reversible] Coercion hset_cartesian_closed_struct_data_to_struct (P : hset_cartesian_closed_struct_data) : hset_cartesian_struct := pr1 P. @@ -177,7 +177,7 @@ Definition hset_cartesian_closed_struct : UU := ∑ (P : hset_cartesian_closed_struct_data), closed_under_fun_laws P. -Coercion hset_cartesian_closed_struct_to_data +#[reversible] Coercion hset_cartesian_closed_struct_to_data (P : hset_cartesian_closed_struct) : hset_cartesian_closed_struct_data := pr1 P. @@ -312,7 +312,7 @@ Definition hset_equalizer_struct : UU := ∑ (EP : hset_equalizer_struct_data P), hset_equalizer_struct_laws EP. -Coercion hset_equalizer_struct_to_data +#[reversible] Coercion hset_equalizer_struct_to_data {P : hset_struct} (EP : hset_equalizer_struct P) : hset_equalizer_struct_data P @@ -450,7 +450,7 @@ Definition hset_coequalizer_struct : UU := ∑ (EP : hset_coequalizer_struct_data P), hset_coequalizer_struct_laws EP. -Coercion hset_coequalizer_struct_to_data +#[reversible] Coercion hset_coequalizer_struct_to_data {P : hset_struct} (EP : hset_coequalizer_struct P) : hset_coequalizer_struct_data P @@ -688,7 +688,7 @@ Definition pointed_hset_struct : UU := ∑ (Pt : pointed_hset_struct_data P), pointed_hset_struct_laws Pt. -Coercion pointed_hset_struct_to_data +#[reversible] Coercion pointed_hset_struct_to_data {P : hset_struct} (Pt : pointed_hset_struct P) : pointed_hset_struct_data P @@ -787,7 +787,7 @@ Definition hset_binary_coprod_struct : UU := ∑ (EP : hset_binary_coprod_struct_data P), hset_binary_coprod_struct_laws EP. -Coercion hset_binary_coprod_struct_to_data +#[reversible] Coercion hset_binary_coprod_struct_to_data {P : hset_struct} (EP : hset_binary_coprod_struct P) : hset_binary_coprod_struct_data P diff --git a/UniMath/CategoryTheory/DisplayedCats/Structures/StructuresSmashProduct.v b/UniMath/CategoryTheory/DisplayedCats/Structures/StructuresSmashProduct.v index 155b2f68c2..7777bdd754 100644 --- a/UniMath/CategoryTheory/DisplayedCats/Structures/StructuresSmashProduct.v +++ b/UniMath/CategoryTheory/DisplayedCats/Structures/StructuresSmashProduct.v @@ -712,7 +712,7 @@ Definition hset_struct_with_smash_closed_adj (** 7. Accessores for structures with an pointed hom-adjunction *) -Coercion hset_struct_with_smash_closed_to_point +#[reversible] Coercion hset_struct_with_smash_closed_to_point {P : hset_cartesian_struct} {Pt : pointed_hset_struct P} {SP : hset_struct_with_smash P Pt} @@ -811,12 +811,12 @@ Definition hset_struct_with_smash_closed (PC : hset_struct_with_smash_closed_adj SP), hset_struct_with_smash_closed_laws_enrich PC. -Coercion hset_struct_with_smash_closed_to_struct +#[reversible] Coercion hset_struct_with_smash_closed_to_struct (PC : hset_struct_with_smash_closed) : hset_cartesian_struct := pr1 PC. -Coercion hset_struct_with_smash_closed_point +#[reversible] Coercion hset_struct_with_smash_closed_point (PC : hset_struct_with_smash_closed) : pointed_hset_struct PC := pr12 PC. diff --git a/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedBinaryCoproducts.v b/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedBinaryCoproducts.v index 8c5f7c3f26..57d83498fa 100644 --- a/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedBinaryCoproducts.v +++ b/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedBinaryCoproducts.v @@ -54,7 +54,7 @@ Section EnrichedCoproducts. × I_{V} --> E ⦃ y , a ⦄. - Coercion ob_enriched_binary_coprod_cocone + #[reversible] Coercion ob_enriched_binary_coprod_cocone (a : enriched_binary_coprod_cocone) : C := pr1 a. @@ -112,12 +112,12 @@ Section EnrichedCoproducts. := ∑ (a : enriched_binary_coprod_cocone), is_binary_coprod_enriched a. - Coercion cone_of_binary_coprod_enriched + #[reversible] Coercion cone_of_binary_coprod_enriched (a : binary_coprod_enriched) : enriched_binary_coprod_cocone := pr1 a. - Coercion binary_coprod_enriched_is_coprod + #[reversible] Coercion binary_coprod_enriched_is_coprod (a : binary_coprod_enriched) : is_binary_coprod_enriched a := pr2 a. @@ -612,7 +612,7 @@ Definition cat_with_enrichment_coproduct : UU := ∑ (C : cat_with_enrichment V), enrichment_binary_coprod C. -Coercion cat_with_enrichment_coproduct_to_cat_with_enrichment +#[reversible] Coercion cat_with_enrichment_coproduct_to_cat_with_enrichment {V : monoidal_cat} (C : cat_with_enrichment_coproduct V) : cat_with_enrichment V diff --git a/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedCoequalizers.v b/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedCoequalizers.v index c67f7a387d..241737ec17 100644 --- a/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedCoequalizers.v +++ b/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedCoequalizers.v @@ -54,7 +54,7 @@ Section EnrichedCoequalizer. (p : I_{V} --> E ⦃ y , a ⦄), f · enriched_to_arr E p = g · enriched_to_arr E p. - Coercion ob_enriched_coequalizer_cocone + #[reversible] Coercion ob_enriched_coequalizer_cocone (a : enriched_coequalizer_cocone) : C := pr1 a. @@ -123,12 +123,12 @@ Section EnrichedCoequalizer. := ∑ (a : enriched_coequalizer_cocone), is_coequalizer_enriched a. - Coercion cocone_of_coequalizer_enriched + #[reversible] Coercion cocone_of_coequalizer_enriched (a : coequalizer_enriched) : enriched_coequalizer_cocone := pr1 a. - Coercion coequalizer_enriched_is_coequalizer + #[reversible] Coercion coequalizer_enriched_is_coequalizer (a : coequalizer_enriched) : is_coequalizer_enriched a := pr2 a. @@ -555,7 +555,7 @@ Definition cat_with_enrichment_coequalizers : UU := ∑ (C : cat_with_enrichment V), enrichment_coequalizers C. -Coercion cat_with_enrichment_coequalizers_to_cat_with_enrichment +#[reversible] Coercion cat_with_enrichment_coequalizers_to_cat_with_enrichment {V : monoidal_cat} (C : cat_with_enrichment_coequalizers V) : cat_with_enrichment V diff --git a/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedColimits.v b/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedColimits.v index 8a32863b92..7e0bda1fb3 100644 --- a/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedColimits.v +++ b/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedColimits.v @@ -58,7 +58,7 @@ Section EnrichedColimit. = #W f · fs j. - Coercion ob_enriched_colim_cocone + #[reversible] Coercion ob_enriched_colim_cocone (a : enriched_colim_cocone) : C := pr1 a. @@ -209,7 +209,7 @@ Section EnrichedColimit. := ∑ (a : enriched_colim_cocone), is_colim_enriched a. - Coercion cocone_of_colim_enriched + #[reversible] Coercion cocone_of_colim_enriched (a : colim_enriched) : enriched_colim_cocone := pr1 a. diff --git a/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedConicalColimits.v b/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedConicalColimits.v index 18530d6273..ceba9f3be9 100644 --- a/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedConicalColimits.v +++ b/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedConicalColimits.v @@ -61,7 +61,7 @@ Section EnrichedConicalColimit. ∏ (i j : I) (f : i --> j), #D f · ps j = ps i. - Coercion ob_enriched_conical_colim_cocone + #[reversible] Coercion ob_enriched_conical_colim_cocone (a : enriched_conical_colim_cocone) : C := pr1 a. @@ -145,12 +145,12 @@ Section EnrichedConicalColimit. := ∑ (a : enriched_conical_colim_cocone), is_conical_colim_enriched a. - Coercion cocone_of_enriched_conical_colim_cocone + #[reversible] Coercion cocone_of_enriched_conical_colim_cocone (a : conical_colim_enriched) : enriched_conical_colim_cocone := pr1 a. - Coercion conical_colim_enriched_is_conical_colim + #[reversible] Coercion conical_colim_enriched_is_conical_colim (a : conical_colim_enriched) : is_conical_colim_enriched a := pr2 a. diff --git a/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedCopowers.v b/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedCopowers.v index 86e82ffd41..1784cbcf7d 100644 --- a/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedCopowers.v +++ b/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedCopowers.v @@ -64,7 +64,7 @@ Section EnrichedCopowers. : UU := ∑ (a : C), v --> E ⦃ x , a ⦄. - Coercion ob_copower_cocone + #[reversible] Coercion ob_copower_cocone (a : copower_cocone) : C := pr1 a. @@ -311,7 +311,7 @@ Definition cat_with_enrichment_copower : UU := ∑ (C : cat_with_enrichment V), enrichment_copower C. -Coercion cat_with_enrichment_copower_to_cat_with_enrichment +#[reversible] Coercion cat_with_enrichment_copower_to_cat_with_enrichment {V : sym_mon_closed_cat} (C : cat_with_enrichment_copower V) : cat_with_enrichment V diff --git a/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedCoproducts.v b/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedCoproducts.v index 602a461037..1d302a2cd5 100644 --- a/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedCoproducts.v +++ b/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedCoproducts.v @@ -47,7 +47,7 @@ Section EnrichedCoproducts. : UU := ∑ (a : C), ∏ (j : J), I_{V} --> E ⦃ D j , a ⦄. - Coercion ob_enriched_coprod_cocone + #[reversible] Coercion ob_enriched_coprod_cocone (a : enriched_coprod_cocone) : C := pr1 a. @@ -96,12 +96,12 @@ Section EnrichedCoproducts. := ∑ (a : enriched_coprod_cocone), is_coprod_enriched a. - Coercion cocone_of_coprod_enriched + #[reversible] Coercion cocone_of_coprod_enriched (a : coprod_enriched) : enriched_coprod_cocone := pr1 a. - Coercion coprod_enriched_is_coprod + #[reversible] Coercion coprod_enriched_is_coprod (a : coprod_enriched) : is_coprod_enriched a := pr2 a. @@ -509,7 +509,7 @@ Definition cat_with_enrichment_coproduct : UU := ∑ (C : cat_with_enrichment V), enrichment_coprod C J. -Coercion cat_with_enrichment_coproduct_to_cat_with_enrichment +#[reversible] Coercion cat_with_enrichment_coproduct_to_cat_with_enrichment {V : monoidal_cat} {J : UU} (C : cat_with_enrichment_coproduct V J) diff --git a/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedInitial.v b/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedInitial.v index 92382e7b6c..2ea37bd8bf 100644 --- a/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedInitial.v +++ b/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedInitial.v @@ -56,12 +56,12 @@ Section EnrichedInitial. : UU := ∑ (x : C), is_initial_enriched x. - Coercion initial_enriched_to_ob + #[reversible] Coercion initial_enriched_to_ob (x : initial_enriched) : C := pr1 x. - Coercion initial_enriched_to_is_initial + #[reversible] Coercion initial_enriched_to_is_initial (x : initial_enriched) : is_initial_enriched x := pr2 x. @@ -229,7 +229,7 @@ Definition cat_with_enrichment_initial : UU := ∑ (C : cat_with_enrichment V), initial_enriched C. -Coercion cat_with_enrichment_initial_to_cat_with_enrichment +#[reversible] Coercion cat_with_enrichment_initial_to_cat_with_enrichment {V : monoidal_cat} (C : cat_with_enrichment_initial V) : cat_with_enrichment V diff --git a/UniMath/CategoryTheory/EnrichedCats/Enrichment.v b/UniMath/CategoryTheory/EnrichedCats/Enrichment.v index 7d7e521402..89ab4f1abc 100644 --- a/UniMath/CategoryTheory/EnrichedCats/Enrichment.v +++ b/UniMath/CategoryTheory/EnrichedCats/Enrichment.v @@ -174,7 +174,7 @@ Definition enrichment : UU := ∑ (E : enrichment_data C V), enrichment_laws E. -Coercion enrichment_to_data +#[reversible] Coercion enrichment_to_data {C : category} {V : monoidal_cat} (E : enrichment C V) @@ -336,13 +336,13 @@ Definition cat_with_enrichment : UU := ∑ (C : category), enrichment C V. -Coercion cat_with_enrichment_to_cat +#[reversible] Coercion cat_with_enrichment_to_cat {V : monoidal_cat} (E : cat_with_enrichment V) : category := pr1 E. -Coercion cat_with_enrichment_to_enrichment +#[reversible] Coercion cat_with_enrichment_to_enrichment {V : monoidal_cat} (E : cat_with_enrichment V) : enrichment E V diff --git a/UniMath/CategoryTheory/EnrichedCats/EnrichmentAdjunction.v b/UniMath/CategoryTheory/EnrichedCats/EnrichmentAdjunction.v index 47c9ae28f2..32c9ab3cc2 100644 --- a/UniMath/CategoryTheory/EnrichedCats/EnrichmentAdjunction.v +++ b/UniMath/CategoryTheory/EnrichedCats/EnrichmentAdjunction.v @@ -116,7 +116,7 @@ Definition enriched_adjunction : UU := ∑ (L : adjunction C₁ C₂), adjunction_enrichment L E₁ E₂. -Coercion enriched_adjunction_to_adjunction +#[reversible] Coercion enriched_adjunction_to_adjunction {V : monoidal_cat} {C₁ C₂ : category} {E₁ : enrichment C₁ V} @@ -125,7 +125,7 @@ Coercion enriched_adjunction_to_adjunction : adjunction C₁ C₂ := pr1 L. -Coercion enriched_adjunction_to_enrichment +#[reversible] Coercion enriched_adjunction_to_enrichment {V : monoidal_cat} {C₁ C₂ : category} {E₁ : enrichment C₁ V} diff --git a/UniMath/CategoryTheory/EnrichedCats/EnrichmentFunctor.v b/UniMath/CategoryTheory/EnrichedCats/EnrichmentFunctor.v index 7462210b55..82ff8a03fb 100644 --- a/UniMath/CategoryTheory/EnrichedCats/EnrichmentFunctor.v +++ b/UniMath/CategoryTheory/EnrichedCats/EnrichmentFunctor.v @@ -172,7 +172,7 @@ Definition functor_with_enrichment : UU := ∑ (F : E₁ ⟶ E₂), functor_enrichment F E₁ E₂. -Coercion functor_with_enrichment_to_functor +#[reversible] Coercion functor_with_enrichment_to_functor {V : monoidal_cat} {E₁ : cat_with_enrichment V} {E₂ : cat_with_enrichment V} diff --git a/UniMath/CategoryTheory/EnrichedCats/EnrichmentMonad.v b/UniMath/CategoryTheory/EnrichedCats/EnrichmentMonad.v index 22518d66fe..fdc3ccebb1 100644 --- a/UniMath/CategoryTheory/EnrichedCats/EnrichmentMonad.v +++ b/UniMath/CategoryTheory/EnrichedCats/EnrichmentMonad.v @@ -39,7 +39,7 @@ Definition monad_enrichment × nat_trans_enrichment (μ M) (functor_comp_enrichment EM EM) EM. -Coercion endo_of_monad_enrichment +#[reversible] Coercion endo_of_monad_enrichment {V : monoidal_cat} {C : category} {E : enrichment C V} @@ -76,7 +76,7 @@ Definition enriched_monad : UU := ∑ (M : Monad C), monad_enrichment E M. -Coercion enriched_monad_to_monad +#[reversible] Coercion enriched_monad_to_monad {V : monoidal_cat} {C : category} {E : enrichment C V} diff --git a/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedBinaryProducts.v b/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedBinaryProducts.v index 55379719d2..13dc7f92f9 100644 --- a/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedBinaryProducts.v +++ b/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedBinaryProducts.v @@ -58,7 +58,7 @@ Section EnrichedProducts. × I_{V} --> E ⦃ a , y ⦄. - Coercion ob_enriched_binary_prod_cone + #[reversible] Coercion ob_enriched_binary_prod_cone (a : enriched_binary_prod_cone) : C := pr1 a. @@ -116,12 +116,12 @@ Section EnrichedProducts. := ∑ (a : enriched_binary_prod_cone), is_binary_prod_enriched a. - Coercion cone_of_binary_prod_enriched + #[reversible] Coercion cone_of_binary_prod_enriched (a : binary_prod_enriched) : enriched_binary_prod_cone := pr1 a. - Coercion binary_prod_enriched_is_prod + #[reversible] Coercion binary_prod_enriched_is_prod (a : binary_prod_enriched) : is_binary_prod_enriched a := pr2 a. @@ -608,7 +608,7 @@ Definition cat_with_enrichment_binary_prod : UU := ∑ (C : cat_with_enrichment V), enrichment_binary_prod C. -Coercion cat_with_enrichment_binary_prod_to_cat_with_enrichment +#[reversible] Coercion cat_with_enrichment_binary_prod_to_cat_with_enrichment {V : monoidal_cat} (C : cat_with_enrichment_binary_prod V) : cat_with_enrichment V diff --git a/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedConicalLimits.v b/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedConicalLimits.v index 8735118add..c80761d98e 100644 --- a/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedConicalLimits.v +++ b/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedConicalLimits.v @@ -60,7 +60,7 @@ Section EnrichedConicalLimit. ∏ (i j : I) (f : i --> j), ps i · #D f = ps j. - Coercion ob_enriched_conical_lim_cone + #[reversible] Coercion ob_enriched_conical_lim_cone (a : enriched_conical_lim_cone) : C := pr1 a. @@ -144,12 +144,12 @@ Section EnrichedConicalLimit. := ∑ (a : enriched_conical_lim_cone), is_conical_lim_enriched a. - Coercion cone_of_conical_lim_enriched + #[reversible] Coercion cone_of_conical_lim_enriched (a : conical_lim_enriched) : enriched_conical_lim_cone := pr1 a. - Coercion enriched_conical_lim_cone_is_conical_lim + #[reversible] Coercion enriched_conical_lim_cone_is_conical_lim (a : conical_lim_enriched) : is_conical_lim_enriched a := pr2 a. diff --git a/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedEqualizers.v b/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedEqualizers.v index dc78808a93..c9691dd0de 100644 --- a/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedEqualizers.v +++ b/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedEqualizers.v @@ -51,7 +51,7 @@ Section EnrichedEqualizer. (p : I_{V} --> E ⦃ a , x ⦄), enriched_to_arr E p · f = enriched_to_arr E p · g. - Coercion ob_enriched_equalizer_cone + #[reversible] Coercion ob_enriched_equalizer_cone (a : enriched_equalizer_cone) : C := pr1 a. @@ -120,12 +120,12 @@ Section EnrichedEqualizer. := ∑ (a : enriched_equalizer_cone), is_equalizer_enriched a. - Coercion cone_of_equalizer_enriched + #[reversible] Coercion cone_of_equalizer_enriched (a : equalizer_enriched) : enriched_equalizer_cone := pr1 a. - Coercion equalizer_enriched_is_equalizer + #[reversible] Coercion equalizer_enriched_is_equalizer (a : equalizer_enriched) : is_equalizer_enriched a := pr2 a. @@ -546,7 +546,7 @@ Definition cat_with_enrichment_equalizers : UU := ∑ (C : cat_with_enrichment V), enrichment_equalizers C. -Coercion cat_with_enrichment_equalizers_to_cat_with_enrichment +#[reversible] Coercion cat_with_enrichment_equalizers_to_cat_with_enrichment {V : monoidal_cat} (C : cat_with_enrichment_equalizers V) : cat_with_enrichment V diff --git a/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedLimits.v b/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedLimits.v index 7b65fb581e..2bc5e4f892 100644 --- a/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedLimits.v +++ b/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedLimits.v @@ -58,7 +58,7 @@ Section EnrichedLimit. = #W f · fs j. - Coercion ob_enriched_lim_cone + #[reversible] Coercion ob_enriched_lim_cone (a : enriched_lim_cone) : C := pr1 a. @@ -217,7 +217,7 @@ Section EnrichedLimit. := ∑ (a : enriched_lim_cone), is_lim_enriched a. - Coercion cone_of_lim_enriched + #[reversible] Coercion cone_of_lim_enriched (a : lim_enriched) : enriched_lim_cone := pr1 a. diff --git a/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedPowers.v b/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedPowers.v index f4ffe19c98..90a451dbe6 100644 --- a/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedPowers.v +++ b/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedPowers.v @@ -54,7 +54,7 @@ Section EnrichedPowers. : UU := ∑ (a : C), v --> E ⦃ a , x ⦄. - Coercion ob_power_cone + #[reversible] Coercion ob_power_cone (a : power_cone) : C := pr1 a. @@ -334,7 +334,7 @@ Definition cat_with_enrichment_power : UU := ∑ (C : cat_with_enrichment V), enrichment_power C. -Coercion cat_with_enrichment_power_to_cat_with_enrichment +#[reversible] Coercion cat_with_enrichment_power_to_cat_with_enrichment {V : sym_mon_closed_cat} (C : cat_with_enrichment_power V) : cat_with_enrichment V diff --git a/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedProducts.v b/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedProducts.v index 7c20565644..76739ab856 100644 --- a/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedProducts.v +++ b/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedProducts.v @@ -46,7 +46,7 @@ Section EnrichedProducts. : UU := ∑ (a : C), ∏ (j : J), I_{V} --> E ⦃ a , D j ⦄. - Coercion ob_enriched_prod_cone + #[reversible] Coercion ob_enriched_prod_cone (a : enriched_prod_cone) : C := pr1 a. @@ -95,12 +95,12 @@ Section EnrichedProducts. := ∑ (a : enriched_prod_cone), is_prod_enriched a. - Coercion cone_of_prod_enriched + #[reversible] Coercion cone_of_prod_enriched (a : prod_enriched) : enriched_prod_cone := pr1 a. - Coercion prod_enriched_is_prod + #[reversible] Coercion prod_enriched_is_prod (a : prod_enriched) : is_prod_enriched a := pr2 a. @@ -501,7 +501,7 @@ Definition cat_with_enrichment_product : UU := ∑ (C : cat_with_enrichment V), enrichment_prod C J. -Coercion cat_with_enrichment_product_to_cat_with_enrichment +#[reversible] Coercion cat_with_enrichment_product_to_cat_with_enrichment {V : monoidal_cat} {J : UU} (C : cat_with_enrichment_product V J) diff --git a/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedTerminal.v b/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedTerminal.v index 4a15caeea9..e277ffbd0d 100644 --- a/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedTerminal.v +++ b/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedTerminal.v @@ -72,12 +72,12 @@ Section EnrichedTerminal. : UU := ∑ (x : C), is_terminal_enriched x. - Coercion terminal_enriched_to_ob + #[reversible] Coercion terminal_enriched_to_ob (x : terminal_enriched) : C := pr1 x. - Coercion terminal_enriched_to_is_terminal + #[reversible] Coercion terminal_enriched_to_is_terminal (x : terminal_enriched) : is_terminal_enriched x := pr2 x. @@ -245,7 +245,7 @@ Definition cat_with_enrichment_terminal : UU := ∑ (C : cat_with_enrichment V), terminal_enriched C. -Coercion cat_with_enrichment_terminal_to_cat_with_enrichment +#[reversible] Coercion cat_with_enrichment_terminal_to_cat_with_enrichment {V : monoidal_cat} (C : cat_with_enrichment_terminal V) : cat_with_enrichment V diff --git a/UniMath/CategoryTheory/Equivalences/CompositesAndInverses.v b/UniMath/CategoryTheory/Equivalences/CompositesAndInverses.v index d7ebaf6ba4..58f29ee485 100644 --- a/UniMath/CategoryTheory/Equivalences/CompositesAndInverses.v +++ b/UniMath/CategoryTheory/Equivalences/CompositesAndInverses.v @@ -43,7 +43,7 @@ Proof. apply (z_iso_is_z_isomorphism (functor_on_z_iso F (make_z_iso' f fH))). Defined. -Coercion left_adj_from_adj_equiv (X Y : category) (K : functor X Y) +#[reversible] Coercion left_adj_from_adj_equiv (X Y : category) (K : functor X Y) (HK : adj_equivalence_of_cats K) : is_left_adjoint K := pr1 HK. (** ** Equivalences *) diff --git a/UniMath/CategoryTheory/Equivalences/Core.v b/UniMath/CategoryTheory/Equivalences/Core.v index d44003e123..854067fed7 100644 --- a/UniMath/CategoryTheory/Equivalences/Core.v +++ b/UniMath/CategoryTheory/Equivalences/Core.v @@ -53,7 +53,7 @@ Definition make_forms_equivalence {A B : category} Definition equivalence_of_cats (A B : category) : UU := ∑ (X : adjunction_data A B), forms_equivalence X. -Coercion adjunction_data_from_equivalence_of_cats {A B} +#[reversible] Coercion adjunction_data_from_equivalence_of_cats {A B} (X : equivalence_of_cats A B) : adjunction_data A B := pr1 X. Definition make_equivalence_of_cats {A B : category} @@ -299,14 +299,14 @@ Section AdjEquiv. := ∑ F : functor A B, adj_equivalence_of_cats F. - Coercion left_adjequiv (A B : category) + #[reversible] Coercion left_adjequiv (A B : category) (F : adj_equiv A B) : functor A B := pr1 F. - Coercion adj_equiv_of_cats_from_adj {A B : category} + #[reversible] Coercion adj_equiv_of_cats_from_adj {A B : category} (E : adj_equiv A B) : adj_equivalence_of_cats E := pr2 E. - Coercion adj_from_adj_equiv {A B} (F : adj_equiv A B) : adjunction A B. + #[reversible] Coercion adj_from_adj_equiv {A B} (F : adj_equiv A B) : adjunction A B. Proof. use make_adjunction. use(make_adjunction_data F). @@ -318,7 +318,7 @@ Section AdjEquiv. + apply triangle_id_right_ad. Defined. - Coercion equiv_from_adj_equiv {A B} (F : adj_equiv A B) : equivalence_of_cats A B. + #[reversible] Coercion equiv_from_adj_equiv {A B} (F : adj_equiv A B) : equivalence_of_cats A B. Proof. use make_equivalence_of_cats. use(make_adjunction_data F). diff --git a/UniMath/CategoryTheory/ExactCategories/ExactCategories.v b/UniMath/CategoryTheory/ExactCategories/ExactCategories.v index c1e353efbb..372b8ae088 100644 --- a/UniMath/CategoryTheory/ExactCategories/ExactCategories.v +++ b/UniMath/CategoryTheory/ExactCategories/ExactCategories.v @@ -155,10 +155,10 @@ Section Pullbacks. (* move upstream *) Local Open Scope type. Definition IsoArrowTo {M : category} {A A' B:M} (g : A --> B) (g' : A' --> B) := ∑ i : z_iso A A', i · g' = g. - Coercion IsoArrowTo_pr1 {M : category} {A A' B:M} (g : A --> B) (g' : A' --> B) : IsoArrowTo g g' -> z_iso A A' := pr1. + #[reversible] Coercion IsoArrowTo_pr1 {M : category} {A A' B:M} (g : A --> B) (g' : A' --> B) : IsoArrowTo g g' -> z_iso A A' := pr1. Definition IsoArrowFrom {M : category} {A B B':M} (g : A --> B) (g' : A --> B') := ∑ i : z_iso B B', g · i = g'. - Coercion IsoArrowFrom_pr1 {M : category} {A B B':M} (g : A --> B) (g' : A --> B') : IsoArrowFrom g g' -> z_iso B B' := pr1. + #[reversible] Coercion IsoArrowFrom_pr1 {M : category} {A B B':M} (g : A --> B) (g' : A --> B') : IsoArrowFrom g g' -> z_iso B B' := pr1. (* this definition of IsoArrow is asymmetric *) Definition IsoArrow {M : category} {A A' B B':M} (g : A --> B) (g' : A' --> B') := ∑ (i : z_iso A A') (j : z_iso B B'), i · g' = g · j. @@ -514,7 +514,7 @@ Section PreAdditive. Definition ismonoidfun_prop {G H:abgr} (f:G->H) : hProp := make_hProp (ismonoidfun f) (isapropismonoidfun f). Definition PreAdditive_functor (M N:PreAdditive) := ∑ F : M ⟶ N, ∀ A B:M, ismonoidfun_prop (@functor_on_morphisms M N F A B : A --> B -> F A --> F B). - Coercion PreAdditive_functor_to_functor {M N:PreAdditive} : PreAdditive_functor M N -> functor M N := pr1. + #[reversible] Coercion PreAdditive_functor_to_functor {M N:PreAdditive} : PreAdditive_functor M N -> functor M N := pr1. Definition functor_on_morphisms_add {C C' : PreAdditive} (F : PreAdditive_functor C C') { a b : C} : monoidfun (a --> b) (F a --> F b) := monoidfunconstr (pr2 F a b). @@ -882,21 +882,21 @@ End KernelCokernelPairs. Section theDefinition. Definition ExactCategoryData := ∑ M:AdditiveCategory, MorphismPair M -> hProp. (* properties added below *) - Coercion ExactCategoryDataToAdditiveCategory (ME : ExactCategoryData) : AdditiveCategory := pr1 ME. + #[reversible] Coercion ExactCategoryDataToAdditiveCategory (ME : ExactCategoryData) : AdditiveCategory := pr1 ME. Definition isExact {M : ExactCategoryData} (E : MorphismPair M) : hProp := pr2 M E. Definition isExact2 {M : ExactCategoryData} {A B C:M} (f:A-->B) (g:B-->C) := isExact (make_MorphismPair f g). Definition isAdmissibleMonomorphism {M : ExactCategoryData} {A B:M} (i : A --> B) : hProp := ∃ C (p : B --> C), isExact2 i p. Definition AdmissibleMonomorphism {M : ExactCategoryData} (A B:M) : Type := ∑ (i : A --> B), isAdmissibleMonomorphism i. - Coercion AdmMonoToMap {M : ExactCategoryData} {A B:M} : AdmissibleMonomorphism A B -> A --> B := pr1. - Coercion AdmMonoToMap' {M : ExactCategoryData} {A B:M} : AdmissibleMonomorphism A B -> (A --> B)%cat := pr1. + #[reversible] Coercion AdmMonoToMap {M : ExactCategoryData} {A B:M} : AdmissibleMonomorphism A B -> A --> B := pr1. + #[reversible] Coercion AdmMonoToMap' {M : ExactCategoryData} {A B:M} : AdmissibleMonomorphism A B -> (A --> B)%cat := pr1. Definition isAdmissibleEpimorphism {M : ExactCategoryData} {B C:M} (p : B --> C) : hProp := ∃ A (i : A --> B), isExact2 i p. Definition AdmissibleEpimorphism {M : ExactCategoryData} (B C:M) : Type := ∑ (p : B --> C), isAdmissibleEpimorphism p. - Coercion AdmEpiToMap {M : ExactCategoryData} {B C:M} : AdmissibleEpimorphism B C -> B --> C := pr1. - Coercion AdmEpiToMap' {M : ExactCategoryData} {B C:M} : AdmissibleEpimorphism B C -> (B --> C)%cat := pr1. + #[reversible] Coercion AdmEpiToMap {M : ExactCategoryData} {B C:M} : AdmissibleEpimorphism B C -> B --> C := pr1. + #[reversible] Coercion AdmEpiToMap' {M : ExactCategoryData} {B C:M} : AdmissibleEpimorphism B C -> (B --> C)%cat := pr1. Lemma ExactToAdmMono {M : ExactCategoryData} {A B C:M} {i : A --> B} {p : B --> C} : isExact2 i p -> isAdmissibleMonomorphism i. Proof. intros e. exact (hinhpr(C,,p,,e)). @@ -947,7 +947,7 @@ Section theDefinition. (∀ (A B C:M) (i:A-->B) (j:B-->C), hasKernel j ⇒ isAdmissibleEpimorphism (i·j) ⇒ isAdmissibleEpimorphism j)). Definition ExactCategory := ∑ (ME:ExactCategoryData), ExactCategoryProperties ME. - Coercion ExactCategoryToData (M:ExactCategory) : ExactCategoryData := pr1 M. + #[reversible] Coercion ExactCategoryToData (M:ExactCategory) : ExactCategoryData := pr1 M. Definition make_ExactCategory (ME:ExactCategoryData) (p : ExactCategoryProperties ME) : ExactCategory := ME,,p. Definition isExactFunctor {M N:ExactCategory} (F : M ⟶ N) : hProp := ∀ (P : MorphismPair M), isExact P ⇒ isExact (applyFunctorToPair F P). @@ -956,11 +956,11 @@ Section theDefinition. (* TO DO : show an exact functor is additive, or else include that as a condition. That includes showing it induces monoid functions on Hom groups. Start by defining preadditive functors and additive functors. *) - Coercion ExactFunctorToFunctor {M N:ExactCategory} + #[reversible] Coercion ExactFunctorToFunctor {M N:ExactCategory} : ExactFunctor M N -> (M ⟶ N) := pr1. Definition ShortExactSequence (M:ExactCategory) := ∑ (P : MorphismPair M), isExact P. - Coercion ShortExactSequenceToMorphismPair {M:ExactCategory} (P : ShortExactSequence M) + #[reversible] Coercion ShortExactSequenceToMorphismPair {M:ExactCategory} (P : ShortExactSequence M) : MorphismPair M := pr1 P. Definition ShortExactSequenceMap {M:ExactCategory} (P Q:ShortExactSequence M) := MorphismPairMap P Q. diff --git a/UniMath/CategoryTheory/FunctorAlgebras.v b/UniMath/CategoryTheory/FunctorAlgebras.v index 2633198355..b0f5ff5884 100644 --- a/UniMath/CategoryTheory/FunctorAlgebras.v +++ b/UniMath/CategoryTheory/FunctorAlgebras.v @@ -124,7 +124,7 @@ Definition is_algebra_mor (X Y : algebra_ob) (f : alg_carrier X --> alg_carrier := alg_map X · f = #F f · alg_map Y. Definition algebra_mor (X Y : algebra_ob) : UU := FunctorAlg⟦X,Y⟧. - Coercion mor_from_algebra_mor {X Y : algebra_ob} (f : algebra_mor X Y) : C⟦X, Y⟧ := pr1 f. + #[reversible] Coercion mor_from_algebra_mor {X Y : algebra_ob} (f : algebra_mor X Y) : C⟦X, Y⟧ := pr1 f. Lemma algebra_mor_commutes (X Y : algebra_ob) (f : algebra_mor X Y) : alg_map X · f = #F f · alg_map Y. diff --git a/UniMath/CategoryTheory/FunctorCoalgebras.v b/UniMath/CategoryTheory/FunctorCoalgebras.v index 5385cc01d4..cd6a1ebd9d 100644 --- a/UniMath/CategoryTheory/FunctorCoalgebras.v +++ b/UniMath/CategoryTheory/FunctorCoalgebras.v @@ -91,7 +91,7 @@ Section Coalgebra_Definition. := coalg_map X · #F f = f · coalg_map Y. Definition coalgebra_mor (X Y : coalgebra_ob) : UU := CoAlg_category⟦X,Y⟧. - Coercion mor_from_coalgebra_mor {X Y : coalgebra_ob} (f : coalgebra_mor X Y) : C⟦X, Y⟧ := pr1 f. + #[reversible] Coercion mor_from_coalgebra_mor {X Y : coalgebra_ob} (f : coalgebra_mor X Y) : C⟦X, Y⟧ := pr1 f. Lemma coalgebra_mor_commutes {X Y : coalgebra_ob} (f : coalgebra_mor X Y) : coalg_map X · #F f = pr1 f · coalg_map Y. diff --git a/UniMath/CategoryTheory/IndexedCategories/IndexedCategory.v b/UniMath/CategoryTheory/IndexedCategories/IndexedCategory.v index 935dbd8e83..ca9650aa54 100644 --- a/UniMath/CategoryTheory/IndexedCategories/IndexedCategory.v +++ b/UniMath/CategoryTheory/IndexedCategories/IndexedCategory.v @@ -168,7 +168,7 @@ Definition make_indexed_cat : indexed_cat C := F ,, HF₁ ,, HF₂. -Coercion indexed_cat_to_data +#[reversible] Coercion indexed_cat_to_data {C : category} (F : indexed_cat C) : indexed_cat_data C diff --git a/UniMath/CategoryTheory/IndexedCategories/IndexedFunctor.v b/UniMath/CategoryTheory/IndexedCategories/IndexedFunctor.v index 54eb67221f..ae90da7eab 100644 --- a/UniMath/CategoryTheory/IndexedCategories/IndexedFunctor.v +++ b/UniMath/CategoryTheory/IndexedCategories/IndexedFunctor.v @@ -132,7 +132,7 @@ Definition make_indexed_functor : indexed_functor Φ Ψ := τ ,, Hτ. -Coercion indexed_functor_to_data +#[reversible] Coercion indexed_functor_to_data {C : category} {Φ Ψ : indexed_cat C} (τ : indexed_functor Φ Ψ) diff --git a/UniMath/CategoryTheory/Limits/Coends.v b/UniMath/CategoryTheory/Limits/Coends.v index e904ec1174..4753ff7755 100644 --- a/UniMath/CategoryTheory/Limits/Coends.v +++ b/UniMath/CategoryTheory/Limits/Coends.v @@ -36,7 +36,7 @@ Section Coends. := ∑ (w : D), ∏ (x : C), F (x ,, x) --> w. - Coercion ob_of_cowedge + #[reversible] Coercion ob_of_cowedge (w : cowedge_data) : D := pr1 w. @@ -66,7 +66,7 @@ Section Coends. : UU := ∑ (w : cowedge_data), is_cowedge w. - Coercion cowedge_data_of_cowedge + #[reversible] Coercion cowedge_data_of_cowedge (w : cowedge) : cowedge_data := pr1 w. @@ -136,7 +136,7 @@ Section Coends. : UU := ∑ (f : w₁ --> w₂), is_cowedge_map f. - Coercion mor_of_cowedge_map + #[reversible] Coercion mor_of_cowedge_map {w₁ w₂ : cowedge} (f : cowedge_map w₁ w₂) : w₁ --> w₂ @@ -194,7 +194,7 @@ Section Coends. : UU := ∑ (w : cowedge), is_coend w. - Coercion coend_colimit_to_cowedge + #[reversible] Coercion coend_colimit_to_cowedge (e : coend_colimit) : cowedge := pr1 e. diff --git a/UniMath/CategoryTheory/Limits/Ends.v b/UniMath/CategoryTheory/Limits/Ends.v index 4bc5348ea5..62d9899be0 100644 --- a/UniMath/CategoryTheory/Limits/Ends.v +++ b/UniMath/CategoryTheory/Limits/Ends.v @@ -38,7 +38,7 @@ Section Ends. := ∑ (w : D), ∏ (x : C), w --> F (x ,, x). - Coercion ob_of_wedge + #[reversible] Coercion ob_of_wedge (w : wedge_data) : D := pr1 w. @@ -68,7 +68,7 @@ Section Ends. : UU := ∑ (w : wedge_data), is_wedge w. - Coercion wedge_data_of_wedge + #[reversible] Coercion wedge_data_of_wedge (w : wedge) : wedge_data := pr1 w. @@ -138,7 +138,7 @@ Section Ends. : UU := ∑ (f : w₁ --> w₂), is_wedge_map f. - Coercion mor_of_wedge_map + #[reversible] Coercion mor_of_wedge_map {w₁ w₂ : wedge} (f : wedge_map w₁ w₂) : w₁ --> w₂ @@ -198,7 +198,7 @@ Section Ends. : UU := ∑ (w : wedge), is_end w. - Coercion end_limit_to_wedge + #[reversible] Coercion end_limit_to_wedge (e : end_limit) : wedge := pr1 e. diff --git a/UniMath/CategoryTheory/Monads/ComonadCoalgebras.v b/UniMath/CategoryTheory/Monads/ComonadCoalgebras.v index 041a5c6482..ecd9b2d007 100644 --- a/UniMath/CategoryTheory/Monads/ComonadCoalgebras.v +++ b/UniMath/CategoryTheory/Monads/ComonadCoalgebras.v @@ -33,7 +33,7 @@ Section Coalgebra_def. Definition Coalgebra_data : UU := ∑ X : C, X --> T X. -Coercion Coalg_carrier (X : Coalgebra_data) : C := pr1 X. +#[reversible] Coercion Coalg_carrier (X : Coalgebra_data) : C := pr1 X. Definition Coalg_map (X : Coalgebra_data) : X --> T X := pr2 X. @@ -43,7 +43,7 @@ Definition Coalgebra_laws (X : Coalgebra_data) : UU Definition Coalgebra : UU := ∑ X : Coalgebra_data, Coalgebra_laws X. -Coercion Coalgebra_data_from_Coalgebra (X : Coalgebra) : Coalgebra_data := pr1 X. +#[reversible] Coercion Coalgebra_data_from_Coalgebra (X : Coalgebra) : Coalgebra_data := pr1 X. Definition Coalgebra_idlaw (X : Coalgebra) : Coalg_map X · ε T X = identity X := pr1 (pr2 X). @@ -75,7 +75,7 @@ Definition is_Coalgebra_mor {X Y : Coalgebra} (f : X --> Y) : UU Definition Coalgebra_mor (X Y : Coalgebra) : UU := ∑ f : X --> Y, is_Coalgebra_mor f. -Coercion mor_from_Coalgebra_mor {X Y : Coalgebra} (f : Coalgebra_mor X Y) +#[reversible] Coercion mor_from_Coalgebra_mor {X Y : Coalgebra} (f : Coalgebra_mor X Y) : X --> Y := pr1 f. Definition Coalgebra_mor_commutes {X Y : Coalgebra} (f : Coalgebra_mor X Y) diff --git a/UniMath/CategoryTheory/Monads/Comonads.v b/UniMath/CategoryTheory/Monads/Comonads.v index 8288a5268f..b2f4c51728 100644 --- a/UniMath/CategoryTheory/Monads/Comonads.v +++ b/UniMath/CategoryTheory/Monads/Comonads.v @@ -115,7 +115,7 @@ Section Comonad_disp_def. Definition Comonad : UU := ob category_Comonad. - Coercion functor_from_Comonad (T : Comonad) : functor C C := pr1 T. + #[reversible] Coercion functor_from_Comonad (T : Comonad) : functor C C := pr1 T. Definition δ (T : Comonad) : T ⟹ T ∙ T := pr112 T. Definition ε (T : Comonad) : T ⟹ functor_identity C := pr212 T. @@ -259,7 +259,7 @@ End pointfree. Definition Comonad_Mor {C : category} (T T' : Comonad C) : UU := category_Comonad C ⟦T, T'⟧. -Coercion nat_trans_from_monad_mor {C : category} (T T' : Comonad C) (s : Comonad_Mor T T') +#[reversible] Coercion nat_trans_from_monad_mor {C : category} (T T' : Comonad C) (s : Comonad_Mor T T') : T ⟹ T' := pr1 s. Definition Comonad_Mor_laws {C : category} {T T' : Comonad C} (α : T ⟹ T') @@ -359,7 +359,7 @@ Section Comonad_eq_helper. (∏ a : ob C, F a --> F (F a))) × (∏ a : ob C, F a --> a)). - Coercion functor_data_from_raw_Comonad_data {C : category} (T : raw_Comonad_data C) : + #[reversible] Coercion functor_data_from_raw_Comonad_data {C : category} (T : raw_Comonad_data C) : functor_data C C := make_functor_data (pr1 T) (pr1 (pr1 (pr2 T))). Definition Comonad'_data_laws {C : category} (T : raw_Comonad_data C) := diff --git a/UniMath/CategoryTheory/Monads/KTriples.v b/UniMath/CategoryTheory/Monads/KTriples.v index a18ba912c3..6d02b51faf 100644 --- a/UniMath/CategoryTheory/Monads/KTriples.v +++ b/UniMath/CategoryTheory/Monads/KTriples.v @@ -78,8 +78,8 @@ Definition η_bind {T : Kleisli_Data} (H : Kleisli_Laws T) : Definition KleisliMonad : UU := ∑ (T : Kleisli_Data), Kleisli_Laws T. (* argument [C] will be set as not implicit after the end of the section *) -Coercion Kleisli_Data_from_Kleisli (T : KleisliMonad) : Kleisli_Data := pr1 T. -Coercion kleisli_laws (T : KleisliMonad) : Kleisli_Laws (pr1 T) := pr2 T. +#[reversible] Coercion Kleisli_Data_from_Kleisli (T : KleisliMonad) : Kleisli_Data := pr1 T. +#[reversible] Coercion kleisli_laws (T : KleisliMonad) : Kleisli_Laws (pr1 T) := pr2 T. End Kleisli_defn. diff --git a/UniMath/CategoryTheory/Monads/Kleisli.v b/UniMath/CategoryTheory/Monads/Kleisli.v index da56aa0023..352c6c7baa 100644 --- a/UniMath/CategoryTheory/Monads/Kleisli.v +++ b/UniMath/CategoryTheory/Monads/Kleisli.v @@ -25,7 +25,7 @@ Proof. apply idpath. Qed. -Coercion RelMonad_from_Kleisli {C : category} (T : KleisliMonad C) := (T : RelMonad (functor_identity C)). +#[reversible] Coercion RelMonad_from_Kleisli {C : category} (T : KleisliMonad C) := (T : RelMonad (functor_identity C)). (** * Equivalence of the types of KleisliMonad and "monoidal" monads *) Section monad_types_equiv. diff --git a/UniMath/CategoryTheory/Monads/LModules.v b/UniMath/CategoryTheory/Monads/LModules.v index 2cac362947..1aca48ef1e 100644 --- a/UniMath/CategoryTheory/Monads/LModules.v +++ b/UniMath/CategoryTheory/Monads/LModules.v @@ -54,7 +54,7 @@ Section LModule_def. Definition LModule_data (D : category) : UU := ∑ F : functor B D, M ∙ F ⟹ F. -Coercion functor_from_LModule_data (C : category) (F : LModule_data C) +#[reversible] Coercion functor_from_LModule_data (C : category) (F : LModule_data C) : functor B C := pr1 F. Definition lm_mult {C : category} (F : LModule_data C) : M ∙ F ⟹ F := pr2 F. @@ -73,7 +73,7 @@ Qed. Definition LModule (C : category) : UU := ∑ T : LModule_data C, LModule_laws T. -Coercion LModule_data_from_LModule (C : category) (T : LModule C) : LModule_data C := pr1 T. +#[reversible] Coercion LModule_data_from_LModule (C : category) (T : LModule C) : LModule_data C := pr1 T. Lemma LModule_law1 {C : category} {T : LModule C} : ∏ c : B, #T (η M c) · σ T c = identity (T c). @@ -109,7 +109,7 @@ Definition LModule_Mor {C : category} (T T' : LModule C) : UU := ∑ α : T ⟹ T', LModule_Mor_laws α. -Coercion nat_trans_from_module_mor (C : category) (T T' : LModule C) (s : LModule_Mor T T') +#[reversible] Coercion nat_trans_from_module_mor (C : category) (T T' : LModule C) (s : LModule_Mor T T') : T ⟹ T' := pr1 s. Definition LModule_Mor_σ {C : category} {T T' : LModule C} (α : LModule_Mor T T') diff --git a/UniMath/CategoryTheory/Monads/MonadAlgebras.v b/UniMath/CategoryTheory/Monads/MonadAlgebras.v index 1ec5f1cb72..49b2280ca2 100644 --- a/UniMath/CategoryTheory/Monads/MonadAlgebras.v +++ b/UniMath/CategoryTheory/Monads/MonadAlgebras.v @@ -40,7 +40,7 @@ Section Algebra_def. Definition Algebra_data : UU := ∑ X : C, T X --> X. -Coercion Alg_carrier (X : Algebra_data) : C := pr1 X. +#[reversible] Coercion Alg_carrier (X : Algebra_data) : C := pr1 X. Definition Alg_map (X : Algebra_data) : T X --> X := pr2 X. @@ -50,7 +50,7 @@ Definition Algebra_laws (X : Algebra_data) : UU Definition Algebra : UU := ∑ X : Algebra_data, Algebra_laws X. -Coercion Algebra_data_from_Algebra (X : Algebra) : Algebra_data := pr1 X. +#[reversible] Coercion Algebra_data_from_Algebra (X : Algebra) : Algebra_data := pr1 X. Definition Algebra_idlaw (X : Algebra) : η T X · Alg_map X = identity X := pr1 (pr2 X). @@ -82,7 +82,7 @@ Definition is_Algebra_mor {X Y : Algebra} (f : X --> Y) : UU Definition Algebra_mor (X Y : Algebra) : UU := ∑ f : X --> Y, is_Algebra_mor f. -Coercion mor_from_Algebra_mor {X Y : Algebra} (f : Algebra_mor X Y) +#[reversible] Coercion mor_from_Algebra_mor {X Y : Algebra} (f : Algebra_mor X Y) : X --> Y := pr1 f. Definition Algebra_mor_commutes {X Y : Algebra} (f : Algebra_mor X Y) diff --git a/UniMath/CategoryTheory/Monads/Monads.v b/UniMath/CategoryTheory/Monads/Monads.v index 0d5d5822a7..21b0fb0efc 100644 --- a/UniMath/CategoryTheory/Monads/Monads.v +++ b/UniMath/CategoryTheory/Monads/Monads.v @@ -134,7 +134,7 @@ Section Monad_disp_def. Definition Monad : UU := ob category_Monad. - Coercion functor_from_Monad (T : Monad) : functor C C := pr1 T. + #[reversible] Coercion functor_from_Monad (T : Monad) : functor C C := pr1 T. Definition μ (T : Monad) : T ∙ T ⟹ T := pr112 T. Definition η (T : Monad) : functor_identity C ⟹ T := pr212 T. @@ -279,7 +279,7 @@ End pointfree. Definition Monad_Mor {C : category} (T T' : Monad C) : UU := category_Monad C ⟦T, T'⟧. -Coercion nat_trans_from_monad_mor {C : category} (T T' : Monad C) (s : Monad_Mor T T') +#[reversible] Coercion nat_trans_from_monad_mor {C : category} (T T' : Monad C) (s : Monad_Mor T T') : T ⟹ T' := pr1 s. Definition Monad_Mor_laws {C : category} {T T' : Monad C} (α : T ⟹ T') @@ -483,7 +483,7 @@ Section Monad_eq_helper. (∏ a : ob C, F (F a) --> F a)) × (∏ a : ob C, a --> F a)). - Coercion functor_data_from_raw_Monad_data {C : category} (T : raw_Monad_data C) : + #[reversible] Coercion functor_data_from_raw_Monad_data {C : category} (T : raw_Monad_data C) : functor_data C C := make_functor_data (pr1 T) (pr1 (pr1 (pr2 T))). Definition Monad'_data_laws {C : category} (T : raw_Monad_data C) := diff --git a/UniMath/CategoryTheory/Monads/RelativeModules.v b/UniMath/CategoryTheory/Monads/RelativeModules.v index fb2438e9bd..01160a9309 100644 --- a/UniMath/CategoryTheory/Monads/RelativeModules.v +++ b/UniMath/CategoryTheory/Monads/RelativeModules.v @@ -78,7 +78,7 @@ Section RelModule_Definition. × (∏ c d e (f : D ⟦J c, R d⟧) (g : D ⟦J d, R e⟧), mbind M f · mbind M g = mbind M (f · r_bind R g)). - Coercion relmonad_axiom_from_relmodule {M : RelModule_data R} (X : RelModule_laws M) + #[reversible] Coercion relmonad_axiom_from_relmodule {M : RelModule_data R} (X : RelModule_laws M) : RelMonad_axioms R := pr1 X. @@ -142,12 +142,12 @@ Definition make_RelModule {C D : precategory_data} {J : C ⟶ D} (R : RelMonad_d : RelModule R := (M,, HM). -Coercion RelModule_data_from_RelModule {C D : precategory_data} {J : C ⟶ D} +#[reversible] Coercion RelModule_data_from_RelModule {C D : precategory_data} {J : C ⟶ D} {R : RelMonad_data J} (M : RelModule R) : RelModule_data R := pr1 M. -Coercion RelModule_laws_from_RelModule {C D : precategory_data} {J : C ⟶ D} +#[reversible] Coercion RelModule_laws_from_RelModule {C D : precategory_data} {J : C ⟶ D} {R : RelMonad_data J} (M : RelModule R) : RelModule_laws M := pr2 M. @@ -228,7 +228,7 @@ Section Part1. := pr1 φ. Coercion relmodule_mor_map : RelModule_Mor >-> Funclass. - Coercion relmodule_mor_property {M N : RelModule R} (φ : RelModule_Mor M N) + #[reversible] Coercion relmodule_mor_property {M N : RelModule R} (φ : RelModule_Mor M N) : is_relmodule_mor M N φ := pr2 φ. @@ -367,4 +367,4 @@ Section Tautological_RelModule. Definition tautological_RelModule : RelModule R := make_RelModule R tautological_RelModule_data tautological_RelModule_law. -End Tautological_RelModule. \ No newline at end of file +End Tautological_RelModule. diff --git a/UniMath/CategoryTheory/Monads/RelativeMonads.v b/UniMath/CategoryTheory/Monads/RelativeMonads.v index bf0e09652d..dfa565abb1 100644 --- a/UniMath/CategoryTheory/Monads/RelativeMonads.v +++ b/UniMath/CategoryTheory/Monads/RelativeMonads.v @@ -73,8 +73,8 @@ Definition r_bind_r_bind {R : RelMonad_data} (X : RelMonad_axioms R) (* implicitness of arguments for RelMonad are set after this section *) Definition RelMonad : UU := ∑ R : RelMonad_data, RelMonad_axioms R. -Coercion RelMonad_data_from_RelMonad (R : RelMonad) : RelMonad_data := pr1 R. -Coercion RelMonad_axioms_from_RelMonad (R : RelMonad) : RelMonad_axioms R := pr2 R. +#[reversible] Coercion RelMonad_data_from_RelMonad (R : RelMonad) : RelMonad_data := pr1 R. +#[reversible] Coercion RelMonad_axioms_from_RelMonad (R : RelMonad) : RelMonad_axioms R := pr2 R. Lemma RelMonad_eq (R R' : RelMonad)(hs : has_homsets D) : pr1 R = pr1 R' -> R = R'. @@ -272,10 +272,10 @@ Definition α_r_bind {C D : precategory_data} {J : functor_data C D} Definition RelMonadMor {C D : precategory_data} {J : functor_data C D} (R R' : RelMonad_data J) : UU := ∑ α : RelMonadMor_data R R', RelMonadMor_axioms α. -Coercion RelMonadMor_data_from_RelMonadMor {C D : precategory_data} {J : functor_data C D} +#[reversible] Coercion RelMonadMor_data_from_RelMonadMor {C D : precategory_data} {J : functor_data C D} {R R' : RelMonad_data J} (α : RelMonadMor R R') : RelMonadMor_data R R' := pr1 α. - Coercion RelMonadMor_axioms_from_RelMonadMor {C D : precategory_data} {J : functor_data C D} + #[reversible] Coercion RelMonadMor_axioms_from_RelMonadMor {C D : precategory_data} {J : functor_data C D} {R R' : RelMonad_data J} (α : RelMonadMor R R') : RelMonadMor_axioms α := pr2 α. diff --git a/UniMath/CategoryTheory/Monoidal/Adjunctions.v b/UniMath/CategoryTheory/Monoidal/Adjunctions.v index 8a3ec355d2..cfc5870b91 100644 --- a/UniMath/CategoryTheory/Monoidal/Adjunctions.v +++ b/UniMath/CategoryTheory/Monoidal/Adjunctions.v @@ -1087,7 +1087,7 @@ Section SymMonoidalAdjunctionAccessors. := pr2 HAA. End SymMonoidalAdjunctionAccessors. -Coercion sym_monoidal_adjunction_to_monoidal_adjunction +#[reversible] Coercion sym_monoidal_adjunction_to_monoidal_adjunction {C₁ C₂ : category} {M₁ : monoidal C₁} {M₂ : monoidal C₂} @@ -1098,7 +1098,7 @@ Coercion sym_monoidal_adjunction_to_monoidal_adjunction : monoidal_adjunction M₁ M₂ A := pr1 HA. -Coercion sym_monoidal_adjunction_to_is_symmetric +#[reversible] Coercion sym_monoidal_adjunction_to_is_symmetric {C₁ C₂ : category} {M₁ : monoidal C₁} {M₂ : monoidal C₂} diff --git a/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/CategoriesOfMonoids.v b/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/CategoriesOfMonoids.v index 063758e110..5fa1a62fda 100644 --- a/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/CategoriesOfMonoids.v +++ b/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/CategoriesOfMonoids.v @@ -51,7 +51,7 @@ Definition is_monoid_mor (X Y : monoid_ob) (f : monoid_carrier X --> monoid_carr Definition monoid_mor (X Y : monoid_ob) : UU := ∑ f : X --> Y, is_monoid_mor X Y f. -Coercion mor_from_monoid_mor (X Y : monoid_ob) (f : monoid_mor X Y) : X --> Y := pr1 f. +#[reversible] Coercion mor_from_monoid_mor (X Y : monoid_ob) (f : monoid_mor X Y) : X --> Y := pr1 f. Definition isaprop_is_monoid_mor (X Y : monoid_ob) (f : monoid_carrier X --> monoid_carrier Y): isaprop (is_monoid_mor X Y f). diff --git a/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/DisplayedMonoidalTensored.v b/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/DisplayedMonoidalTensored.v index 37f92ab0ee..e85c9d13a8 100644 --- a/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/DisplayedMonoidalTensored.v +++ b/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/DisplayedMonoidalTensored.v @@ -764,7 +764,7 @@ Section section_tensor. Definition monoidal_tensor_section : UU := ∑ (α : monoidal_tensor_section_data), monoidal_tensor_section_natural α. - Coercion monoidal_tensor_section_data_from_monoidal_tensor_section (α : monoidal_tensor_section) + #[reversible] Coercion monoidal_tensor_section_data_from_monoidal_tensor_section (α : monoidal_tensor_section) : monoidal_tensor_section_data := pr1 α. diff --git a/UniMath/CategoryTheory/Monoidal/Categories.v b/UniMath/CategoryTheory/Monoidal/Categories.v index 54eb49422a..97046e8158 100644 --- a/UniMath/CategoryTheory/Monoidal/Categories.v +++ b/UniMath/CategoryTheory/Monoidal/Categories.v @@ -423,7 +423,7 @@ Definition monoidal_tensor_is_bifunctor : is_bifunctor M := pr12 M. -Coercion monoidal_tensor +#[reversible] Coercion monoidal_tensor {C : category} (M : monoidal C) : bifunctor C C C @@ -1308,8 +1308,8 @@ Local Open Scope moncat. Definition monoidal_cat : UU := ∑ (C : category), monoidal C. -Coercion monoidal_cat_to_cat (V : monoidal_cat) : category := pr1 V. -Coercion monoidal_cat_to_monoidal (V : monoidal_cat) : monoidal V := pr2 V. +#[reversible] Coercion monoidal_cat_to_cat (V : monoidal_cat) : category := pr1 V. +#[reversible] Coercion monoidal_cat_to_monoidal (V : monoidal_cat) : monoidal V := pr2 V. Definition monoidal_cat_tensor_pt {V : monoidal_cat} diff --git a/UniMath/CategoryTheory/Monoidal/FunctorCategories.v b/UniMath/CategoryTheory/Monoidal/FunctorCategories.v index 4ea4885519..1518e55159 100644 --- a/UniMath/CategoryTheory/Monoidal/FunctorCategories.v +++ b/UniMath/CategoryTheory/Monoidal/FunctorCategories.v @@ -193,7 +193,7 @@ Definition category_symmetric_monoidal_comonad : category Definition symmetric_monoidal_comonad : UU := ob category_symmetric_monoidal_comonad. -Coercion comonad_from_symmetric_monoidal_comonad (T : symmetric_monoidal_comonad) +#[reversible] Coercion comonad_from_symmetric_monoidal_comonad (T : symmetric_monoidal_comonad) : Comonad C := pr11 T ,, pr12 T. diff --git a/UniMath/CategoryTheory/Monoidal/Functors.v b/UniMath/CategoryTheory/Monoidal/Functors.v index 1de7805ae8..e717924d4f 100644 --- a/UniMath/CategoryTheory/Monoidal/Functors.v +++ b/UniMath/CategoryTheory/Monoidal/Functors.v @@ -1487,13 +1487,13 @@ Definition lax_monoidal_functor : UU := ∑ (F : V₁ ⟶ V₂), fmonoidal_lax V₁ V₂ F. -Coercion lax_monoidal_functor_to_functor +#[reversible] Coercion lax_monoidal_functor_to_functor {V₁ V₂ : monoidal_cat} (F : lax_monoidal_functor V₁ V₂) : V₁ ⟶ V₂ := pr1 F. -Coercion lax_monoidal_functor_to_fmonoidal_lax +#[reversible] Coercion lax_monoidal_functor_to_fmonoidal_lax {V₁ V₂ : monoidal_cat} (F : lax_monoidal_functor V₁ V₂) : fmonoidal_lax V₁ V₂ F @@ -1505,7 +1505,7 @@ Definition symmetric_lax_monoidal_functor := ∑ (F : lax_monoidal_functor V₁ V₂), is_symmetric_monoidal_functor (pr2 V₁) (pr2 V₂) (pr2 F). -Coercion symmetric_lax_monoidal_functor_to_lax_monoidal +#[reversible] Coercion symmetric_lax_monoidal_functor_to_lax_monoidal {V₁ V₂ : sym_monoidal_cat} (F : symmetric_lax_monoidal_functor V₁ V₂) : lax_monoidal_functor V₁ V₂ @@ -1516,7 +1516,7 @@ Definition strong_monoidal_functor : UU := ∑ (F : V₁ ⟶ V₂), fmonoidal V₁ V₂ F. -Coercion strong_monoidal_functor_to_lax_monoidal_functor +#[reversible] Coercion strong_monoidal_functor_to_lax_monoidal_functor {V₁ V₂ : monoidal_cat} (F : strong_monoidal_functor V₁ V₂) : lax_monoidal_functor V₁ V₂ @@ -1528,13 +1528,13 @@ Definition symmetric_strong_monoidal_functor := ∑ (F : strong_monoidal_functor V₁ V₂), is_symmetric_monoidal_functor (pr2 V₁) (pr2 V₂) (pr2 F). -Coercion symmetric_strong_monoidal_functor_to_strong_monoidal +#[reversible] Coercion symmetric_strong_monoidal_functor_to_strong_monoidal {V₁ V₂ : sym_monoidal_cat} (F : symmetric_strong_monoidal_functor V₁ V₂) : strong_monoidal_functor V₁ V₂ := pr1 F. -Coercion symmetric_strong_monoidal_functor_to_lax_symmetric +#[reversible] Coercion symmetric_strong_monoidal_functor_to_lax_symmetric {V₁ V₂ : sym_monoidal_cat} (F : symmetric_strong_monoidal_functor V₁ V₂) : symmetric_lax_monoidal_functor V₁ V₂ diff --git a/UniMath/CategoryTheory/Monoidal/StrongMonad.v b/UniMath/CategoryTheory/Monoidal/StrongMonad.v index 2c1899f3b2..4f9ec2a1ca 100644 --- a/UniMath/CategoryTheory/Monoidal/StrongMonad.v +++ b/UniMath/CategoryTheory/Monoidal/StrongMonad.v @@ -130,7 +130,7 @@ Section LeftStrength. : UU := ∑ (tM : left_strength M), left_strong_monad_laws tM. - Coercion left_strong_monad_strength + #[reversible] Coercion left_strong_monad_strength {M : Monad V} (tM : left_strong_monad M) : left_strength M diff --git a/UniMath/CategoryTheory/Monoidal/Structure/Cartesian.v b/UniMath/CategoryTheory/Monoidal/Structure/Cartesian.v index e98da36385..49a0a8a76b 100644 --- a/UniMath/CategoryTheory/Monoidal/Structure/Cartesian.v +++ b/UniMath/CategoryTheory/Monoidal/Structure/Cartesian.v @@ -84,7 +84,7 @@ Definition is_cartesian : UU := ∑ (HM : is_semicartesian M), tensor_isBinProduct HM. -Coercion is_cartesian_to_semicartesian +#[reversible] Coercion is_cartesian_to_semicartesian {M : monoidal_cat} (M_cart : is_cartesian M) : is_semicartesian M @@ -486,7 +486,7 @@ Definition is_cocartesian : UU := ∑ (HM : is_semicocartesian M), tensor_isBinCoproduct HM. -Coercion is_cocartesian_to_semicocartesian +#[reversible] Coercion is_cocartesian_to_semicocartesian {M : monoidal_cat} (M_cocart : is_cocartesian M) : is_semicocartesian M diff --git a/UniMath/CategoryTheory/Monoidal/Structure/Closed.v b/UniMath/CategoryTheory/Monoidal/Structure/Closed.v index df1c65da4f..9fcf027bef 100644 --- a/UniMath/CategoryTheory/Monoidal/Structure/Closed.v +++ b/UniMath/CategoryTheory/Monoidal/Structure/Closed.v @@ -99,7 +99,7 @@ Definition sym_mon_closed_cat : UU := ∑ (V : sym_monoidal_cat), monoidal_leftclosed V. -Coercion sym_monoidal_closed_cat_to_sym_monoidal_cat +#[reversible] Coercion sym_monoidal_closed_cat_to_sym_monoidal_cat (V : sym_mon_closed_cat) : sym_monoidal_cat := pr1 V. diff --git a/UniMath/CategoryTheory/Monoidal/Structure/Symmetric.v b/UniMath/CategoryTheory/Monoidal/Structure/Symmetric.v index e818117952..44bfe0a5cd 100644 --- a/UniMath/CategoryTheory/Monoidal/Structure/Symmetric.v +++ b/UniMath/CategoryTheory/Monoidal/Structure/Symmetric.v @@ -312,12 +312,12 @@ Definition sym_monoidal_cat : UU := ∑ (V : monoidal_cat), symmetric V. -Coercion sym_monoidal_cat_to_monoidal_cat +#[reversible] Coercion sym_monoidal_cat_to_monoidal_cat (V : sym_monoidal_cat) : monoidal_cat := pr1 V. -Coercion sym_monoidal_cat_to_symmetric +#[reversible] Coercion sym_monoidal_cat_to_symmetric (V : sym_monoidal_cat) : symmetric V := pr2 V. diff --git a/UniMath/CategoryTheory/PointedFunctors.v b/UniMath/CategoryTheory/PointedFunctors.v index fb2af92252..b003e91e22 100644 --- a/UniMath/CategoryTheory/PointedFunctors.v +++ b/UniMath/CategoryTheory/PointedFunctors.v @@ -36,7 +36,7 @@ Context (C : category). Definition ptd_obj : UU := ∑ F : functor C C, functor_identity C ⟹ F. -Coercion functor_from_ptd_obj (F : ptd_obj) : functor C C := pr1 F. +#[reversible] Coercion functor_from_ptd_obj (F : ptd_obj) : functor C C := pr1 F. Definition ptd_pt (F : ptd_obj) : functor_identity C ⟹ F := pr2 F. @@ -45,7 +45,7 @@ Definition is_ptd_mor {F G : ptd_obj}(α: F ⟹ G) : UU := ∏ c : C, ptd_pt F c Definition ptd_mor (F G : ptd_obj) : UU := ∑ α : F ⟹ G, is_ptd_mor α. -Coercion nat_trans_from_ptd_mor {F G : ptd_obj} (a : ptd_mor F G) : nat_trans F G := pr1 a. +#[reversible] Coercion nat_trans_from_ptd_mor {F G : ptd_obj} (a : ptd_mor F G) : nat_trans F G := pr1 a. Lemma eq_ptd_mor {F G : ptd_obj} (a b : ptd_mor F G) : a = b ≃ (a : F ⟹ G) = b. diff --git a/UniMath/CategoryTheory/Profunctors/Squares.v b/UniMath/CategoryTheory/Profunctors/Squares.v index 7dcd8bcc4f..dede994b8e 100644 --- a/UniMath/CategoryTheory/Profunctors/Squares.v +++ b/UniMath/CategoryTheory/Profunctors/Squares.v @@ -147,7 +147,7 @@ Definition profunctor_iso_square : UU := ∑ (τ : profunctor_square F G P Q), is_profunctor_nat_iso τ. -Coercion profunctor_iso_square_to_square +#[reversible] Coercion profunctor_iso_square_to_square {C₁ C₂ D₁ D₂ : category} {F : C₁ ⟶ C₂} {G : D₁ ⟶ D₂} @@ -157,7 +157,7 @@ Coercion profunctor_iso_square_to_square : profunctor_square F G P Q := pr1 τ. -Coercion profunctor_iso_square_is_iso +#[reversible] Coercion profunctor_iso_square_is_iso {C₁ C₂ D₁ D₂ : category} {F : C₁ ⟶ C₂} {G : D₁ ⟶ D₂} diff --git a/UniMath/CategoryTheory/Profunctors/Transformation.v b/UniMath/CategoryTheory/Profunctors/Transformation.v index 0325a38103..bc10f058ee 100644 --- a/UniMath/CategoryTheory/Profunctors/Transformation.v +++ b/UniMath/CategoryTheory/Profunctors/Transformation.v @@ -311,14 +311,14 @@ Definition make_profunctor_nat_iso : profunctor_nat_iso P Q := τ ,, Hτ. -Coercion profunctor_nat_iso_to_profunctor_nat_trans +#[reversible] Coercion profunctor_nat_iso_to_profunctor_nat_trans {C₁ C₂ : category} {P Q : profunctor C₁ C₂} (τ : profunctor_nat_iso P Q) : profunctor_nat_trans P Q := pr1 τ. -Coercion profunctor_nat_iso_to_is_profunctor_nat_iso +#[reversible] Coercion profunctor_nat_iso_to_is_profunctor_nat_iso {C₁ C₂ : category} {P Q : profunctor C₁ C₂} (τ : profunctor_nat_iso P Q) diff --git a/UniMath/CategoryTheory/Retracts.v b/UniMath/CategoryTheory/Retracts.v index 8048ae134e..e2b2fa3e87 100644 --- a/UniMath/CategoryTheory/Retracts.v +++ b/UniMath/CategoryTheory/Retracts.v @@ -102,7 +102,7 @@ Section Idempotents. : UU := ∑ (e : c --> c), is_idempotent e. - Coercion idempotent_morphism + #[reversible] Coercion idempotent_morphism {c : C} (e : idempotent c) : c --> c @@ -125,7 +125,7 @@ Section Idempotents. : UU := ∑ (e : c --> c), is_split_idempotent e. - Coercion split_idempotent_morphism + #[reversible] Coercion split_idempotent_morphism {c : C} (e : split_idempotent c) : c --> c diff --git a/UniMath/CategoryTheory/SkewMonoidal/CategoriesOfMonoids.v b/UniMath/CategoryTheory/SkewMonoidal/CategoriesOfMonoids.v index 454a5cc474..a606167c4c 100644 --- a/UniMath/CategoryTheory/SkewMonoidal/CategoriesOfMonoids.v +++ b/UniMath/CategoryTheory/SkewMonoidal/CategoriesOfMonoids.v @@ -34,7 +34,7 @@ Notation ρ' := (skewmonoidal_unitr (data_from_skewmonoidal V)). Definition skewMonoid_data : UU := ∑ X : V, (X ⊗ X --> X) × (I --> X). -Coercion sm_ob (X : skewMonoid_data) : V := pr1 X. +#[reversible] Coercion sm_ob (X : skewMonoid_data) : V := pr1 X. Definition sm_unit (X : skewMonoid_data) : I --> X := pr2 (pr2 X). Definition sm_mult (X : skewMonoid_data) : X ⊗ X --> X := pr1 (pr2 X). @@ -48,7 +48,7 @@ Definition skewMonoid_laws (X : skewMonoid_data) : UU := Definition skewMonoid : UU := ∑ (X : skewMonoid_data), skewMonoid_laws X. -Coercion skewMonoid_to_data (X : skewMonoid) : skewMonoid_data := pr1 X. +#[reversible] Coercion skewMonoid_to_data (X : skewMonoid) : skewMonoid_data := pr1 X. Definition skewMonoid_pentagon (X : skewMonoid) : μ X #⊗ identity X · μ X = α' X X X · identity X #⊗ μ X · μ X @@ -76,7 +76,7 @@ Qed. Definition skewMonoid_Mor (T T' : skewMonoid_data) : UU := ∑ α , @skewMonoid_Mor_laws T T' α. -Coercion mor_from_monoid_mor (T T' : skewMonoid_data) (s : skewMonoid_Mor T T') +#[reversible] Coercion mor_from_monoid_mor (T T' : skewMonoid_data) (s : skewMonoid_Mor T T') : V ⟦ T , T' ⟧ := pr1 s. Definition skewMonoid_Mor_η {T T' : skewMonoid_data } (α : skewMonoid_Mor T T') diff --git a/UniMath/CategoryTheory/SkewMonoidal/SkewMonoidalCategories.v b/UniMath/CategoryTheory/SkewMonoidal/SkewMonoidalCategories.v index 0427fa4e47..0dbf307f92 100644 --- a/UniMath/CategoryTheory/SkewMonoidal/SkewMonoidalCategories.v +++ b/UniMath/CategoryTheory/SkewMonoidal/SkewMonoidalCategories.v @@ -39,7 +39,7 @@ Definition skewmonoidal_data : UU := (precategory_binproduct_unassoc _ _ _) ∙ (functor_identity V × tensor)%F ∙ tensor . -Coercion cat_from_skewmonoidal (V : skewmonoidal_data) : category := pr1 V. +#[reversible] Coercion cat_from_skewmonoidal (V : skewmonoidal_data) : category := pr1 V. Definition skewmonoidal_tensor (V : skewmonoidal_data) : V ⊠ V ⟶ V := pr1 (pr2 V). @@ -113,7 +113,7 @@ Definition skewmonoidal_category : UU := α' a b c #⊗ id d · α' a (b ⊗ c) d · id a #⊗ α' b c d). -Coercion data_from_skewmonoidal (V : skewmonoidal_category) : skewmonoidal_data := pr1 V. +#[reversible] Coercion data_from_skewmonoidal (V : skewmonoidal_category) : skewmonoidal_data := pr1 V. Local Notation eq := (pr2 (_ : skewmonoidal_category)). diff --git a/UniMath/CategoryTheory/TwoSidedDisplayedCats/DisplayedFunctor.v b/UniMath/CategoryTheory/TwoSidedDisplayedCats/DisplayedFunctor.v index 723868675c..a73f1b9980 100644 --- a/UniMath/CategoryTheory/TwoSidedDisplayedCats/DisplayedFunctor.v +++ b/UniMath/CategoryTheory/TwoSidedDisplayedCats/DisplayedFunctor.v @@ -126,7 +126,7 @@ Section DisplayedFunctor. : UU := ∑ (FG : twosided_disp_functor_data), twosided_disp_functor_laws FG. - Coercion twosided_disp_functor_to_data + #[reversible] Coercion twosided_disp_functor_to_data (FG : twosided_disp_functor) : twosided_disp_functor_data := pr1 FG. diff --git a/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Lenses.v b/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Lenses.v index 995e45d61c..a9fa092448 100644 --- a/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Lenses.v +++ b/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Lenses.v @@ -364,7 +364,7 @@ Section Lenses. : lens_data s v := get ,, put. - Coercion lens_to_data + #[reversible] Coercion lens_to_data {s v : C} (l : lens s v) : lens_data s v diff --git a/UniMath/CategoryTheory/TwoSidedDisplayedCats/Isos.v b/UniMath/CategoryTheory/TwoSidedDisplayedCats/Isos.v index 432f1ca649..c03c3f2a89 100644 --- a/UniMath/CategoryTheory/TwoSidedDisplayedCats/Isos.v +++ b/UniMath/CategoryTheory/TwoSidedDisplayedCats/Isos.v @@ -72,7 +72,7 @@ Definition iso_twosided_disp := ∑ (fg : xy₁ -->[ f ][ g ] xy₂), is_iso_twosided_disp (pr2 f) (pr2 g) fg. -Coercion iso_twosided_disp_to_mor +#[reversible] Coercion iso_twosided_disp_to_mor {C₁ C₂ : category} {D : twosided_disp_cat C₁ C₂} {x₁ x₂ : C₁} @@ -85,7 +85,7 @@ Coercion iso_twosided_disp_to_mor : xy₁ -->[ f ][ g ] xy₂ := pr1 fg. -Coercion iso_twosided_disp_to_mor_is_iso +#[reversible] Coercion iso_twosided_disp_to_mor_is_iso {C₁ C₂ : category} {D : twosided_disp_cat C₁ C₂} {x₁ x₂ : C₁} diff --git a/UniMath/CategoryTheory/TwoSidedDisplayedCats/Strictness.v b/UniMath/CategoryTheory/TwoSidedDisplayedCats/Strictness.v index abeac937ec..9097ce99fb 100644 --- a/UniMath/CategoryTheory/TwoSidedDisplayedCats/Strictness.v +++ b/UniMath/CategoryTheory/TwoSidedDisplayedCats/Strictness.v @@ -54,7 +54,7 @@ Definition strict_twosided_disp_cat : UU := ∑ (D : twosided_disp_cat C₁ C₂), is_strict_twosided_disp_cat D. -Coercion strict_twosided_disp_cat_to_twosided_disp_cat +#[reversible] Coercion strict_twosided_disp_cat_to_twosided_disp_cat {C₁ C₂ : category} (D : strict_twosided_disp_cat C₁ C₂) : twosided_disp_cat C₁ C₂ diff --git a/UniMath/CategoryTheory/TwoSidedDisplayedCats/TwoSidedDispCat.v b/UniMath/CategoryTheory/TwoSidedDisplayedCats/TwoSidedDispCat.v index 76329cee5e..08d7df1dae 100644 --- a/UniMath/CategoryTheory/TwoSidedDisplayedCats/TwoSidedDispCat.v +++ b/UniMath/CategoryTheory/TwoSidedDisplayedCats/TwoSidedDispCat.v @@ -186,7 +186,7 @@ Definition twosided_disp_cat_data := ∑ (D : twosided_disp_cat_ob_mor C₁ C₂), twosided_disp_cat_id_comp D. -Coercion twosided_disp_cat_data_to_twosided_disp_cat_ob_mor +#[reversible] Coercion twosided_disp_cat_data_to_twosided_disp_cat_ob_mor {C₁ C₂ : precategory_data} (D : twosided_disp_cat_data) : twosided_disp_cat_ob_mor C₁ C₂ @@ -446,7 +446,7 @@ Section TwoSidedDispCat. := ∑ (D : twosided_disp_cat_data), twosided_disp_cat_axioms D. - Coercion twosided_disp_cat_to_twosided_disp_cat_data + #[reversible] Coercion twosided_disp_cat_to_twosided_disp_cat_data (D : twosided_disp_cat) : twosided_disp_cat_data := pr1 D. diff --git a/UniMath/CategoryTheory/TwoSidedDisplayedCats/Univalence.v b/UniMath/CategoryTheory/TwoSidedDisplayedCats/Univalence.v index cfab6cf765..c11f08910a 100644 --- a/UniMath/CategoryTheory/TwoSidedDisplayedCats/Univalence.v +++ b/UniMath/CategoryTheory/TwoSidedDisplayedCats/Univalence.v @@ -118,7 +118,7 @@ Definition univalent_twosided_disp_cat : UU := ∑ (D : twosided_disp_cat C₁ C₂), is_univalent_twosided_disp_cat D. -Coercion univalent_twosided_disp_cat_to_twosided_disp_cat +#[reversible] Coercion univalent_twosided_disp_cat_to_twosided_disp_cat {C₁ C₂ : category} (D : univalent_twosided_disp_cat C₁ C₂) : twosided_disp_cat C₁ C₂ diff --git a/UniMath/CategoryTheory/rezk_completion.v b/UniMath/CategoryTheory/rezk_completion.v index 9f313bf237..e3498739eb 100644 --- a/UniMath/CategoryTheory/rezk_completion.v +++ b/UniMath/CategoryTheory/rezk_completion.v @@ -82,7 +82,7 @@ End rezk. Definition functor_from (C : precategory) : UU := ∑ D : univalent_category, functor C D. -Coercion target_category (C : precategory) (X : functor_from C) : univalent_category := pr1 X. +#[reversible] Coercion target_category (C : precategory) (X : functor_from C) : univalent_category := pr1 X. Definition func_functor_from {C : precategory} (X : functor_from C) : functor C X := pr2 X. Definition is_initial_functor_from (C : precategory) (X : functor_from C) : UU diff --git a/UniMath/Combinatorics/MetricTree.v b/UniMath/Combinatorics/MetricTree.v index 793e413f8d..698ec1f42b 100644 --- a/UniMath/Combinatorics/MetricTree.v +++ b/UniMath/Combinatorics/MetricTree.v @@ -17,7 +17,7 @@ Definition Tree : Type := (mt_symm: ∏ x y, mt_dist x y = mt_dist y x) (mt_trans: ∏ x y z, mt_dist x z <= mt_dist x y + mt_dist y z), (* mt_step: *) ∏ x z, x != z -> ∑ y, (S (mt_dist x y) = mt_dist x z) × (mt_dist y z = 1). -Coercion mt_set (x:Tree) := pr1 x. +#[reversible] Coercion mt_set (x:Tree) := pr1 x. Definition mt_dist (x:Tree) := pr12 x. Definition mt_refl (x:Tree) := pr122 x. Definition mt_anti (x:Tree) := pr122 (pr2 x). diff --git a/UniMath/Induction/FunctorAlgebras_legacy.v b/UniMath/Induction/FunctorAlgebras_legacy.v index 49615e68b4..933f94eb05 100644 --- a/UniMath/Induction/FunctorAlgebras_legacy.v +++ b/UniMath/Induction/FunctorAlgebras_legacy.v @@ -75,7 +75,7 @@ Definition is_algebra_mor (X Y : algebra_ob) (f : alg_carrier X --> alg_carrier Definition algebra_mor (X Y : algebra_ob) : UU := ∑ f : X --> Y, is_algebra_mor X Y f. -Coercion mor_from_algebra_mor (X Y : algebra_ob) (f : algebra_mor X Y) : X --> Y := pr1 f. +#[reversible] Coercion mor_from_algebra_mor (X Y : algebra_ob) (f : algebra_mor X Y) : X --> Y := pr1 f. Lemma algebra_mor_commutes (X Y : algebra_ob) (f : algebra_mor X Y) diff --git a/UniMath/Induction/W/Wtypes.v b/UniMath/Induction/W/Wtypes.v index acaaca5b36..9bb82b21b3 100644 --- a/UniMath/Induction/W/Wtypes.v +++ b/UniMath/Induction/W/Wtypes.v @@ -1,10 +1,10 @@ (** * Axiomatic definition of a W-type. *) -(** -Gianluca Amato, Matteo Calosci, Marco Maggesi, Cosimo Perini Brogi 2019-2024. +(** +Gianluca Amato, Matteo Calosci, Marco Maggesi, Cosimo Perini Brogi 2019-2024. Derived from the code in the GitHub repository ## https://github.com/HoTT/Archive/tree/master/LICS2012 ##, which accompanies the paper -"_Inductive Types in Homotopy Type Theory_", by S. Awodey, N. Gambino and K. Sojakova. +"_Inductive Types in Homotopy Type Theory_", by S. Awodey, N. Gambino and K. Sojakova. *) Require Import UniMath.Foundations.All. @@ -22,7 +22,7 @@ Definition Wtype (A: UU) (B: ∏ x: A, UU): UU (x : A) (f : B x → U) , w_ind P e_s (w_sup x f) = e_s x f (λ u, w_ind P e_s (f u))). -Coercion w_carrier {A: UU} {B: ∏ x: A, UU} (W: Wtype A B): UU := pr1 W. +#[reversible] Coercion w_carrier {A: UU} {B: ∏ x: A, UU} (W: Wtype A B): UU := pr1 W. Section W. @@ -66,7 +66,7 @@ Proof. - etrans. all: revgoals. * apply pathsinv0. - apply w_beta. + apply w_beta. * apply maponpaths. apply funextsec. intro. @@ -78,7 +78,7 @@ Defined. Definition w_eta_2 (P: W → UU) (e_s: ∏ (x: A) (f: B x → W) (IH: ∏ u: B x, P (f u)), P (w_sup x f)) (h: ∏ x: W, P x) (p_s: ∏ (x: A) (f: B x → W), h (w_sup x f) = (e_s x f (λ b, h (f b)))) : ∏ (x : A) (f : B x → W) - , w_eta_1 P e_s h p_s (w_sup x f) @ w_beta P e_s x f + , w_eta_1 P e_s h p_s (w_sup x f) @ w_beta P e_s x f = p_s x f @ maponpaths (e_s x f) (funextsec _ _ _ (fun b => w_eta_1 P e_s h p_s (f b))). Proof. intros. diff --git a/UniMath/ModelCategories/Generated/GenericFreeMonoid.v b/UniMath/ModelCategories/Generated/GenericFreeMonoid.v index d01ab0da6e..092cc18f5b 100644 --- a/UniMath/ModelCategories/Generated/GenericFreeMonoid.v +++ b/UniMath/ModelCategories/Generated/GenericFreeMonoid.v @@ -29,17 +29,17 @@ Context {C : category} (V : monoidal C). Definition pointed : UU := ∑ T, I_{V} --> T. -Coercion pointed_obj (T : pointed) : C := pr1 T. +#[reversible] Coercion pointed_obj (T : pointed) : C := pr1 T. Definition pointed_pt (T : pointed) : I_{V} --> T := pr2 T. Definition Mon_alg_data (T : pointed) (A : C) : UU := - ∑ (a : T ⊗_{V} A --> A), + ∑ (a : T ⊗_{V} A --> A), (luinv_{V} _) · ((pointed_pt T) ⊗^{V}_{r} A) · a = identity _. -Coercion Mon_alg_map {T : pointed} {X : C} (XX : Mon_alg_data T X) := pr1 XX. +#[reversible] Coercion Mon_alg_map {T : pointed} {X : C} (XX : Mon_alg_data T X) := pr1 XX. Definition Mon_alg_map_comm {T : pointed} {X : C} (XX : Mon_alg_data T X) := pr2 XX. -Definition Mon_alg_mor_axioms +Definition Mon_alg_mor_axioms {T : pointed} {X Y : C} (XX : Mon_alg_data T X) @@ -47,12 +47,12 @@ Definition Mon_alg_mor_axioms (f : X --> Y) : UU := XX · f = (T ⊗^{V}_{l} f) · YY. -Lemma isaprop_Mon_alg_mor_axioms +Lemma isaprop_Mon_alg_mor_axioms {T : pointed} {X Y : C} (XX : Mon_alg_data T X) (YY : Mon_alg_data T Y) - (f : X --> Y) : + (f : X --> Y) : isaprop (Mon_alg_mor_axioms XX YY f). Proof. apply homset_property. @@ -67,7 +67,7 @@ Proof. exact (Mon_alg_mor_axioms XX YY f). Defined. -Definition Mon_alg_disp_id_comp (T : pointed) : +Definition Mon_alg_disp_id_comp (T : pointed) : disp_cat_id_comp _ (Mon_alg_disp_ob_mor T). Proof. split. @@ -89,15 +89,15 @@ Proof. etrans. apply assoc'. etrans. apply cancel_precomposition. exact gg. - + apply pathsinv0. etrans. apply maponpaths_2. use (bifunctor_leftcomp V). apply assoc'. (* Qed because morphisms are propositional anyway *) -Qed. +Qed. -Definition Mon_alg_disp_data (T : pointed) : +Definition Mon_alg_disp_data (T : pointed) : disp_cat_data C := (_,, Mon_alg_disp_id_comp T). Definition Mon_alg_axioms (T : pointed) : @@ -108,13 +108,13 @@ Proof. apply homset_property. Defined. -Definition Mon_alg_disp (T : pointed) : +Definition Mon_alg_disp (T : pointed) : disp_cat C := (_,, Mon_alg_axioms T). -Definition Mon_alg (T : pointed) : +Definition Mon_alg (T : pointed) : category := total_category (Mon_alg_disp T). -Lemma Mon_alg_action_alg_map_rel {T : pointed} +Lemma Mon_alg_action_alg_map_rel {T : pointed} (X : Mon_alg T) (A : C) : luinv^{ V }_{ pr1 X ⊗_{ V} A} · pointed_pt T ⊗^{ V}_{r} (pr1 X ⊗_{ V} A) · (αinv^{ V }_{ T, pr1 X, A} · pr12 X ⊗^{ V}_{r} A) = @@ -132,16 +132,16 @@ Proof. etrans. apply maponpaths_2. apply maponpaths. exact associnvnat. - + etrans. apply cancel_postcomposition. apply assoc. etrans. do 2 apply cancel_postcomposition. exact trinv. - + etrans. apply cancel_postcomposition. exact (pathsinv0 (whiskerrightcomp A _ _ _ _ _)). etrans. exact (pathsinv0 (whiskerrightcomp A _ _ _ _ _)). - + etrans. apply maponpaths. exact xrel. apply (bifunctor_rightid V). @@ -151,7 +151,7 @@ Lemma Mon_alg_action_mor_rel {T : pointed} (X : Mon_alg T) {A B : C} (f : A --> B) : Mon_alg_mor_axioms (_,, Mon_alg_action_alg_map_rel X A) - (_,, Mon_alg_action_alg_map_rel X B) (pr1 X ⊗^{ V}_{l} f). + (_,, Mon_alg_action_alg_map_rel X B) (pr1 X ⊗^{ V}_{l} f). Proof. (* unfold Mon_alg_mor_axioms. *) destruct X as [X [x xrel]]. @@ -213,10 +213,10 @@ Definition Mon_alg_forgetful_functor (T : pointed) : (* todo: show that this holds whenever sequence on I --> X converges *) Definition alg_forgetful_functor_right_action_is_adjoint {T : pointed} (X : Mon_alg T) : UU := - are_adjoints (Mon_alg_right_action X) (Mon_alg_forgetful_functor T). + are_adjoints (Mon_alg_right_action X) (Mon_alg_forgetful_functor T). (* not every object can be pointed in a general monoidal category *) -Definition alg_forgetful_functor_right_action_is_adjoint_induced_mul {T : pointed} (X : Mon_alg T) +Definition alg_forgetful_functor_right_action_is_adjoint_induced_mul {T : pointed} (X : Mon_alg T) (Adj : alg_forgetful_functor_right_action_is_adjoint X) : (pr1 X) ⊗_{V} (pr1 X) --> (pr1 X). Proof. @@ -232,7 +232,7 @@ Proof. Defined. Definition alg_forgetful_functor_right_action_is_adjoint_monoid_data - {T : pointed} {X : Mon_alg T} + {T : pointed} {X : Mon_alg T} (Adj : alg_forgetful_functor_right_action_is_adjoint X) : monoid_data V (pr1 X). Proof. @@ -242,49 +242,49 @@ Proof. Defined. Definition alg_forgetful_functor_right_action_adjoint_monad_unit_preserves_right_tensor - {T : pointed} {X : Mon_alg T} + {T : pointed} {X : Mon_alg T} (Adj : alg_forgetful_functor_right_action_is_adjoint X) := let m := Monad_from_adjunction Adj in - ∏ (Y : C), - η m Y = - luinv_{V} Y · + ∏ (Y : C), + η m Y = + luinv_{V} Y · η m I_{V} ⊗^{V}_{r} Y · (ru_{V} (pr1 X)) ⊗^{V}_{r} Y. -(* need: -pr1 X ⊗^{ V}_{l} (pr1 X ⊗^{ V}_{l} ruinv^{ V }_{ pr1 X}) · μ m (m I_{ V}) +(* need: +pr1 X ⊗^{ V}_{l} (pr1 X ⊗^{ V}_{l} ruinv^{ V }_{ pr1 X}) · μ m (m I_{ V}) = αinv^{ V }_{ pr1 X, pr1 X, pr1 X} · (pr1 X ⊗^{ V}_{l} ruinv^{ V }_{ pr1 X} · μ (Monad_from_adjunction Adj) I_{ V} · ru^{ V }_{ pr1 X}) ⊗^{ V}_{r} pr1 X · pr1 X ⊗^{ V}_{l} ruinv^{ V }_{ pr1 X} *) Definition alg_forgetful_functor_right_action_adjoint_monad_mul_preserves_right_tensor - {T : pointed} {X : Mon_alg T} + {T : pointed} {X : Mon_alg T} (Adj : alg_forgetful_functor_right_action_is_adjoint X) := let m := Monad_from_adjunction Adj in - ∏ (Y : C), - μ m Y = + ∏ (Y : C), + μ m Y = αinv_{V} _ _ _ · (_ ⊗^{V}_{l} ruinv_{V} _) ⊗^{V}_{r} _ · μ m I_{V} ⊗^{V}_{r} Y · ru_{V} _ ⊗^{V}_{r} _. (* Definition alg_forgetful_functor_right_action_adjoint_monad_mul_preserves_right_tensor - {T : pointed} {X : Mon_alg T} + {T : pointed} {X : Mon_alg T} (Adj : alg_forgetful_functor_right_action_is_adjoint X) := let m := Monad_from_adjunction Adj in - ∏ (Y : C), - μ m Y = - (pr1 X) ⊗^{V}_{l} ((pr1 X) ⊗^{V}_{l} luinv_{V} Y) · - (pr1 X) ⊗^{V}_{l} αinv_{V} _ _ _ · - αinv_{V} _ _ _ · + ∏ (Y : C), + μ m Y = + (pr1 X) ⊗^{V}_{l} ((pr1 X) ⊗^{V}_{l} luinv_{V} Y) · + (pr1 X) ⊗^{V}_{l} αinv_{V} _ _ _ · + αinv_{V} _ _ _ · μ m I_{V} ⊗^{V}_{r} Y · (α_{V} _ _ _) · (pr1 X) ⊗^{V}_{l} lu_{V} Y. *) -Definition alg_forgetful_functor_right_action_is_adjoint_monoid_laws - {T : pointed} {X : Mon_alg T} +Definition alg_forgetful_functor_right_action_is_adjoint_monoid_laws + {T : pointed} {X : Mon_alg T} {Adj : alg_forgetful_functor_right_action_is_adjoint X} (ηr : alg_forgetful_functor_right_action_adjoint_monad_unit_preserves_right_tensor Adj) (μr : alg_forgetful_functor_right_action_adjoint_monad_mul_preserves_right_tensor Adj) : @@ -294,12 +294,12 @@ Proof. set (m := Monad_from_adjunction Adj). set (u := unit_from_are_adjoints Adj). repeat split. - - + - (* unfold monoid_laws_unit_left. cbn. unfold alg_forgetful_functor_right_action_is_adjoint_induced_mul. *) (* cbn. *) - + etrans. apply maponpaths_2. apply (bifunctor_rightcomp V). etrans. apply assoc. @@ -308,7 +308,7 @@ Proof. etrans. do 2 apply cancel_postcomposition. apply maponpaths. apply (whiskerscommutes _ (bifunctor_equalwhiskers V)). - + etrans. do 2 apply cancel_postcomposition. { etrans. apply assoc. @@ -319,13 +319,13 @@ Proof. (* transform rhs to identity (m I_{V}) (== identity (pr1 X)) then plug in monad law 1 *) apply pathsinv0. - apply (pre_comp_with_z_iso_is_inj + apply (pre_comp_with_z_iso_is_inj (is_inverse_in_precat_inv (monoidal_leftunitorisolaw V _))). - apply (pre_comp_with_z_iso_is_inj + apply (pre_comp_with_z_iso_is_inj (monoidal_rightunitorisolaw V _)). - apply (post_comp_with_z_iso_is_inj + apply (post_comp_with_z_iso_is_inj (is_inverse_in_precat_inv (monoidal_rightunitorisolaw V (pr1 X)))). - etrans. + etrans. { etrans. apply cancel_postcomposition. apply cancel_precomposition. @@ -335,9 +335,9 @@ Proof. etrans. apply (monoidal_rightunitorisolaw V _). exact (pathsinv0 (Monad_law1 (T := m) I_{V})). } - + (* cbn. *) - + apply pathsinv0. etrans. apply cancel_postcomposition, assoc. etrans. apply cancel_postcomposition, assoc. @@ -362,7 +362,7 @@ Proof. etrans. apply cancel_postcomposition. apply (monoidal_rightunitorisolaw V _). apply id_left. - - + - (* unfold monoid_laws_unit_right. cbn. unfold alg_forgetful_functor_right_action_is_adjoint_induced_mul. @@ -375,7 +375,7 @@ Proof. etrans. do 2 apply cancel_postcomposition. etrans. apply assoc'. apply cancel_precomposition. - { + { etrans. apply (pathsinv0 (bifunctor_leftcomp V _ _ _ _ _ _)). etrans. apply maponpaths. exact (pr1 (monoidal_rightunitorisolaw V (pr1 X))). @@ -383,13 +383,13 @@ Proof. } etrans. do 2 apply cancel_postcomposition. apply id_right. - + apply pathsinv0. etrans. apply (pathsinv0 (id_left _)). apply cancel_postcomposition. apply pathsinv0. exact (Monad_law2 (T := m) I_{V}). - - + - (* unfold monoid_laws_assoc. *) (* cbn. *) (* unfold alg_forgetful_functor_right_action_is_adjoint_induced_mul. *) @@ -424,7 +424,7 @@ Proof. apply (bifunctor_leftid V). etrans. do 2 apply cancel_postcomposition. apply id_right. - + etrans. do 2 apply cancel_postcomposition. apply assoc. etrans. apply cancel_postcomposition. @@ -433,7 +433,7 @@ Proof. apply cancel_precomposition. (* #m (μ m I_{V}) = X ⊗^{V}_{l} μ m I_{V} *) exact (Monad_law3 (T := m) I_{V}). - + (* cbn. *) etrans. apply maponpaths_2. apply assoc. @@ -444,7 +444,7 @@ Proof. apply cancel_postcomposition. apply pathsinv0. - apply (pre_comp_with_z_iso_is_inj + apply (pre_comp_with_z_iso_is_inj (is_inverse_in_precat_inv (monoidal_associatorisolaw V _ _ _))). etrans. apply assoc. etrans. apply cancel_postcomposition, assoc. @@ -452,12 +452,12 @@ Proof. apply (monoidal_associatorisolaw V). etrans. apply assoc'. etrans. apply id_left. - + etrans. apply maponpaths. apply μr. etrans. apply assoc. etrans. apply cancel_postcomposition, assoc. - + apply pathsinv0. etrans. apply assoc. etrans. apply cancel_postcomposition. @@ -474,7 +474,7 @@ Proof. apply (whiskerscommutes _ (bifunctor_equalwhiskers V)). etrans. apply assoc. apply cancel_postcomposition. - + etrans. apply assoc'. etrans. apply cancel_precomposition. { @@ -487,7 +487,7 @@ Proof. etrans. apply cancel_postcomposition. apply (pathsinv0 (monoidal_associatorinvnatleftright V _ _ _ _ _)). - + apply pathsinv0. etrans. apply cancel_precomposition. apply (pathsinv0 (monoidal_associatorinvnatleftright V _ _ _ _ _)). @@ -508,8 +508,8 @@ Proof. apply (monoidal_associatorinvnatleft V). Qed. -Definition alg_forgetful_functor_right_action_is_adjoint_monoid - {T : pointed} {X : Mon_alg T} +Definition alg_forgetful_functor_right_action_is_adjoint_monoid + {T : pointed} {X : Mon_alg T} {Adj : alg_forgetful_functor_right_action_is_adjoint X} (ηr : alg_forgetful_functor_right_action_adjoint_monad_unit_preserves_right_tensor Adj) (μr : alg_forgetful_functor_right_action_adjoint_monad_mul_preserves_right_tensor Adj) : @@ -520,7 +520,7 @@ Definition alg_forgetful_functor_right_action_is_adjoint_monoid alg_forgetful_functor_right_action_is_adjoint X -> (total_category (NWFS C)). Proof. intro Adj. - + exists (pr11 X). split; [exact (pr21 X)|]. @@ -528,4 +528,4 @@ Proof. exact (alg_forgetful_functor_right_action_is_adjoint_monad_laws Adj). Defined. *) -End Mon_alg. \ No newline at end of file +End Mon_alg. diff --git a/UniMath/ModelCategories/Generated/GenericFreeMonoidSequence.v b/UniMath/ModelCategories/Generated/GenericFreeMonoidSequence.v index 7dfbeaf30a..5056b51a85 100644 --- a/UniMath/ModelCategories/Generated/GenericFreeMonoidSequence.v +++ b/UniMath/ModelCategories/Generated/GenericFreeMonoidSequence.v @@ -58,7 +58,7 @@ Local Definition pair_diagram_lob (X : pair_diagram) : C := pr1 X. Local Definition pair_diagram_rob (X : pair_diagram) : C := pr12 X. -Coercion pair_diagram_arr (X : pair_diagram) := +#[reversible] Coercion pair_diagram_arr (X : pair_diagram) := pr22 X. Local Definition pair_diagram_horizontal_arrow (X : pair_diagram) : (pair_diagram_lob X) --> (pair_diagram_rob X). diff --git a/UniMath/ModelCategories/Generated/LiftingWithClass.v b/UniMath/ModelCategories/Generated/LiftingWithClass.v index 1dad166127..defa30431c 100644 --- a/UniMath/ModelCategories/Generated/LiftingWithClass.v +++ b/UniMath/ModelCategories/Generated/LiftingWithClass.v @@ -48,7 +48,7 @@ Context {C : category}. Definition morcls_disp (J : morphism_class C) : disp_cat (arrow C) := disp_full_sub (arrow C) (λ g, J _ _ g). -Coercion total_morcls_disp_arrow +#[reversible] Coercion total_morcls_disp_arrow {J : morphism_class C} (g : total_category (morcls_disp J)) := pr1 g. @@ -130,7 +130,7 @@ Definition rlp_morcls (J : morphism_class C) : category := Definition morcls_lp (J : morphism_class C) (f : arrow C) : UU := ∑ (g : total_category (morcls_disp J)), (pr1 g) --> f. -Coercion morcls_lp_diagram {J : morphism_class C} {f : arrow C} (lp : morcls_lp J f) := pr2 lp. +#[reversible] Coercion morcls_lp_diagram {J : morphism_class C} {f : arrow C} (lp : morcls_lp J f) := pr2 lp. Definition morcls_lp_map {J : morphism_class C} {f : arrow C} (lp : morcls_lp J f) := pr1 lp. Context (n : nwfs C). diff --git a/UniMath/ModelCategories/NWFS.v b/UniMath/ModelCategories/NWFS.v index 7754ab7851..3be774a5bc 100644 --- a/UniMath/ModelCategories/NWFS.v +++ b/UniMath/ModelCategories/NWFS.v @@ -271,7 +271,7 @@ Defined. *) (* We can't really do this with the "naive definition" of three C, since then we need the middle object for the section. We would have to define our own theory. *) Definition functorial_factorization (C : category) := section_disp (three_disp C). -Coercion fact_section {C : category} (F : functorial_factorization C) +#[reversible] Coercion fact_section {C : category} (F : functorial_factorization C) := section_disp_data_from_section_disp F. Definition fact_functor {C : category} (F : functorial_factorization C) : arrow C ⟶ three C := section_functor F. diff --git a/UniMath/OrderTheory/DCPOs/AlternativeDefinitions/FixedPointTheorems.v b/UniMath/OrderTheory/DCPOs/AlternativeDefinitions/FixedPointTheorems.v index 3033dcd7da..a62aba39b6 100644 --- a/UniMath/OrderTheory/DCPOs/AlternativeDefinitions/FixedPointTheorems.v +++ b/UniMath/OrderTheory/DCPOs/AlternativeDefinitions/FixedPointTheorems.v @@ -378,7 +378,7 @@ Section Least. : least_of_family p -> I := pr1. (* Would be nice to make [least_of_family_index] a coercion, but can’t since its target is an arbitrary type. The best we can do instead is [realise_least_of_family]: *) - Coercion realise_least_of_family {I} (p : I -> P) + #[reversible] Coercion realise_least_of_family {I} (p : I -> P) : least_of_family p -> P := fun ih => p (pr1 ih). @@ -437,7 +437,7 @@ Section Greatest. : greatest_of_family p -> I := pr1. (* Would be nice to make [greatest_of_family_index] a coercion, but can’t since its target is an arbitrary type. The best we can do instead is [realise_greatest_of_family]: *) - Coercion realise_greatest_of_family {I} (p : I -> P) + #[reversible] Coercion realise_greatest_of_family {I} (p : I -> P) : greatest_of_family p -> P := fun ih => p (pr1 ih). @@ -597,7 +597,7 @@ Section Chains. Definition Chain (P : Poset) : UU := ∑ (I : UU), ∑ (p : I -> P), is_chain p. - Coercion chain_index {P} (C : Chain P) : UU + #[reversible] Coercion chain_index {P} (C : Chain P) : UU := pr1 C. Definition chain_family {P} (C : Chain P) : C -> P @@ -627,10 +627,10 @@ Section Chains. Definition Chain_hsubtype (P : Poset) : UU := ∑ A : hsubtype P, is_chain (pr1carrier A). - Coercion pr1_Chain_hsubtype {P} : Chain_hsubtype P -> hsubtype P + #[reversible] Coercion pr1_Chain_hsubtype {P} : Chain_hsubtype P -> hsubtype P := pr1. - Coercion Chain_of_Chain_hsubtype (P : Poset) + #[reversible] Coercion Chain_of_Chain_hsubtype (P : Poset) : Chain_hsubtype P -> Chain P. Proof. intros C. exact (carrier C,, (pr1carrier C,, pr2 C)). @@ -659,7 +659,7 @@ Section Directed. Definition Directed_family (P : Poset) : UU := ∑ (I : UU), ∑ (p : I -> P), isdirected p. - Coercion directed_index {P} (C : Directed_family P) : UU + #[reversible] Coercion directed_index {P} (C : Directed_family P) : UU := pr1 C. Definition directed_family {P} (C : Directed_family P) : C -> P @@ -698,10 +698,10 @@ Section Directed. Definition Directed_hsubtype (P : Poset) : UU := ∑ A : hsubtype P, isdirected (pr1carrier A). - Coercion pr1_Directed_hsubtype {P} : Directed_hsubtype P -> hsubtype P + #[reversible] Coercion pr1_Directed_hsubtype {P} : Directed_hsubtype P -> hsubtype P := pr1. - Coercion Directed_of_Directed_hsubtype (P : Poset) + #[reversible] Coercion Directed_of_Directed_hsubtype (P : Poset) : Directed_hsubtype P -> Directed_family P. Proof. intros C. exact (carrier C,, (pr1carrier C,, pr2 C)). @@ -1017,7 +1017,7 @@ Definition isfixedpoint {P : Poset} (f : P -> P) : hsubtype P Definition Fixedpoint {P : Poset} (f : P -> P) : UU := carrier (isfixedpoint f). -Coercion pr1_Fixedpoint {P : Poset} {f : P -> P} : Fixedpoint f -> P +#[reversible] Coercion pr1_Fixedpoint {P : Poset} {f : P -> P} : Fixedpoint f -> P := pr1carrier _. Definition fixedpoint_property {P : Poset} {f : P -> P} (x : Fixedpoint f) @@ -1030,7 +1030,7 @@ Definition ispostfixedpoint {P : Poset} (f : P -> P) : hsubtype P Definition Postfixedpoint {P : Poset} (f : P -> P) : UU := carrier (ispostfixedpoint f). -Coercion pr1_Postfixedpoint {P : Poset} {f : P -> P} : Postfixedpoint f -> P +#[reversible] Coercion pr1_Postfixedpoint {P : Poset} {f : P -> P} : Postfixedpoint f -> P := pr1carrier _. Definition postfixedpoint_property {P : Poset} {f : P -> P} (x : Postfixedpoint f) diff --git a/UniMath/OrderTheory/DCPOs/Basis/Basis.v b/UniMath/OrderTheory/DCPOs/Basis/Basis.v index cadd7c06e5..03013d9045 100644 --- a/UniMath/OrderTheory/DCPOs/Basis/Basis.v +++ b/UniMath/OrderTheory/DCPOs/Basis/Basis.v @@ -62,7 +62,7 @@ Section BasisInDCPO. : UU := ∑ (B : UU), B → X. - Coercion dcpo_basis_data_to_type + #[reversible] Coercion dcpo_basis_data_to_type (B : dcpo_basis_data) : UU := pr1 B. @@ -114,12 +114,12 @@ Section BasisInDCPO. : dcpo_basis := B ,, HB. - Coercion dcpo_basis_to_data + #[reversible] Coercion dcpo_basis_to_data (B : dcpo_basis) : dcpo_basis_data := pr1 B. - Coercion dcpo_basis_to_laws + #[reversible] Coercion dcpo_basis_to_laws (B : dcpo_basis) : dcpo_basis_laws B := pr2 B. diff --git a/UniMath/OrderTheory/DCPOs/Basis/CompactBasis.v b/UniMath/OrderTheory/DCPOs/Basis/CompactBasis.v index 68c34bcc88..bb6e488c61 100644 --- a/UniMath/OrderTheory/DCPOs/Basis/CompactBasis.v +++ b/UniMath/OrderTheory/DCPOs/Basis/CompactBasis.v @@ -79,12 +79,12 @@ Section CompactBasisInDCPO. : compact_basis := B ,, HB. - Coercion compact_basis_to_data + #[reversible] Coercion compact_basis_to_data (B : compact_basis) : dcpo_basis_data X := pr1 B. - Coercion compact_basis_to_laws + #[reversible] Coercion compact_basis_to_laws (B : compact_basis) : compact_basis_laws B := pr2 B. diff --git a/UniMath/OrderTheory/DCPOs/Core/Basics.v b/UniMath/OrderTheory/DCPOs/Core/Basics.v index ab79deecf5..12a6a46aa2 100644 --- a/UniMath/OrderTheory/DCPOs/Core/Basics.v +++ b/UniMath/OrderTheory/DCPOs/Core/Basics.v @@ -78,7 +78,7 @@ Section Upperbounds. : lub := x ,, Hx. - Coercion lub_to_el + #[reversible] Coercion lub_to_el (x : lub) : X := pr1 x. @@ -178,7 +178,7 @@ Proof. apply isaprop_directed_complete_poset. Qed. -Coercion dcpo_struct_to_PartialOrder +#[reversible] Coercion dcpo_struct_to_PartialOrder {X : hSet} (DX : dcpo_struct X) : PartialOrder X @@ -200,9 +200,9 @@ Definition dcpo : UU := ∑ (X : hSet), dcpo_struct X. -Coercion dcpo_to_hSet (X : dcpo) : hSet := pr1 X. +#[reversible] Coercion dcpo_to_hSet (X : dcpo) : hSet := pr1 X. -Coercion dcpo_to_PartialOrder (X : dcpo) : PartialOrder X := pr12 X. +#[reversible] Coercion dcpo_to_PartialOrder (X : dcpo) : PartialOrder X := pr12 X. Definition dcpo_order {X : dcpo} (x y : X) : hProp := pr12 X x y. @@ -364,13 +364,13 @@ Definition dcppo_struct : UU := ∑ (DX : dcpo_struct X), bottom_element DX. -Coercion dcppo_struct_to_dcpo_struct +#[reversible] Coercion dcppo_struct_to_dcpo_struct {X : hSet} (DX : dcppo_struct X) : dcpo_struct X := pr1 DX. -Coercion dcppo_to_pointed_PartialOrder +#[reversible] Coercion dcppo_to_pointed_PartialOrder {X : hSet} (DX : dcppo_struct X) : pointed_PartialOrder X @@ -391,7 +391,7 @@ Definition dcppo : UU := ∑ (X : hSet), dcppo_struct X. -Coercion dcppo_to_dcpo +#[reversible] Coercion dcppo_to_dcpo (X : dcppo) : dcpo := pr1 X ,, pr12 X. diff --git a/UniMath/OrderTheory/DCPOs/Core/DirectedSets.v b/UniMath/OrderTheory/DCPOs/Core/DirectedSets.v index 3580f41f70..602d6fc51e 100644 --- a/UniMath/OrderTheory/DCPOs/Core/DirectedSets.v +++ b/UniMath/OrderTheory/DCPOs/Core/DirectedSets.v @@ -62,7 +62,7 @@ Definition directed_set (** 2. Accessors and builders *) -Coercion directed_set_dom +#[reversible] Coercion directed_set_dom {X : hSet} {PX : PartialOrder X} (D : directed_set PX) diff --git a/UniMath/OrderTheory/DCPOs/Core/ScottContinuous.v b/UniMath/OrderTheory/DCPOs/Core/ScottContinuous.v index ad448dbe96..28748089ef 100644 --- a/UniMath/OrderTheory/DCPOs/Core/ScottContinuous.v +++ b/UniMath/OrderTheory/DCPOs/Core/ScottContinuous.v @@ -58,7 +58,7 @@ Definition is_strict_scott_continuous × f (pointed_PartialOrder_to_point DX) = pointed_PartialOrder_to_point DY. -Coercion is_strict_scott_continuous_to_scott_continuous +#[reversible] Coercion is_strict_scott_continuous_to_scott_continuous {X Y : hSet} {DX : dcppo_struct X} {DY : dcppo_struct Y} @@ -366,7 +366,7 @@ Definition strict_scott_continuous_map : UU := ∑ (f : X → Y), is_strict_scott_continuous X Y f. -Coercion strict_scott_continuous_map_to_scott_continuous_map +#[reversible] Coercion strict_scott_continuous_map_to_scott_continuous_map {X Y : dcppo} (f : strict_scott_continuous_map X Y) : scott_continuous_map X Y @@ -409,7 +409,7 @@ Proof. exact p. Qed. -Coercion scott_continuous_map_to_monotone +#[reversible] Coercion scott_continuous_map_to_monotone {X Y : dcpo} (f : scott_continuous_map X Y) : monotone_function X Y. diff --git a/UniMath/OrderTheory/DCPOs/Core/ScottTopology.v b/UniMath/OrderTheory/DCPOs/Core/ScottTopology.v index 94639af303..14dbe6d9f3 100644 --- a/UniMath/OrderTheory/DCPOs/Core/ScottTopology.v +++ b/UniMath/OrderTheory/DCPOs/Core/ScottTopology.v @@ -90,7 +90,7 @@ Definition scott_open_set_to_pred Coercion scott_open_set_to_pred : scott_open_set >-> Funclass. -Coercion is_scott_open_scott_open_set +#[reversible] Coercion is_scott_open_scott_open_set {X : dcpo} (P : scott_open_set X) : is_scott_open P @@ -110,7 +110,7 @@ Definition scott_closed_set_to_pred Coercion scott_closed_set_to_pred : scott_closed_set >-> Funclass. -Coercion is_scott_closed_scott_closed_set +#[reversible] Coercion is_scott_closed_scott_closed_set {X : dcpo} (P : scott_closed_set X) : is_scott_closed P diff --git a/UniMath/OrderTheory/DCPOs/Elements/Maximal.v b/UniMath/OrderTheory/DCPOs/Elements/Maximal.v index f6200c63c9..3716749617 100644 --- a/UniMath/OrderTheory/DCPOs/Elements/Maximal.v +++ b/UniMath/OrderTheory/DCPOs/Elements/Maximal.v @@ -235,7 +235,7 @@ Definition strongly_maximal : hSet := (∑ (x : X), hProp_to_hSet (is_strongly_maximal x))%set. -Coercion element_of_strongly_maximal +#[reversible] Coercion element_of_strongly_maximal {X : dcpo} (x : strongly_maximal X) : X diff --git a/UniMath/OrderTheory/DCPOs/Examples/IdealCompletion.v b/UniMath/OrderTheory/DCPOs/Examples/IdealCompletion.v index 8179274963..8539e9a08a 100644 --- a/UniMath/OrderTheory/DCPOs/Examples/IdealCompletion.v +++ b/UniMath/OrderTheory/DCPOs/Examples/IdealCompletion.v @@ -55,7 +55,7 @@ Definition abstract_basis_data : UU := ∑ (X : UU), X → X → hProp. -Coercion type_of_abstract_basis_data +#[reversible] Coercion type_of_abstract_basis_data (B : abstract_basis_data) : UU := pr1 B. @@ -94,7 +94,7 @@ Definition make_abstract_basis : abstract_basis := B ,, HB. -Coercion abstract_basis_to_data +#[reversible] Coercion abstract_basis_to_data (B : abstract_basis) : abstract_basis_data := pr1 B. diff --git a/UniMath/OrderTheory/DCPOs/FixpointTheorems/Pataraia.v b/UniMath/OrderTheory/DCPOs/FixpointTheorems/Pataraia.v index 6b76f89957..5e52ce698a 100644 --- a/UniMath/OrderTheory/DCPOs/FixpointTheorems/Pataraia.v +++ b/UniMath/OrderTheory/DCPOs/FixpointTheorems/Pataraia.v @@ -56,7 +56,7 @@ Definition progressive_map : UU := ∑ (f : monotone_function X X), is_progressive f. -Coercion monotone_function_of_progressive_map +#[reversible] Coercion monotone_function_of_progressive_map {X : dcpo} (f : progressive_map X) : monotone_function X X diff --git a/UniMath/OrderTheory/Posets/PointedPosets.v b/UniMath/OrderTheory/Posets/PointedPosets.v index bd2a2a9829..ae90e7ea76 100644 --- a/UniMath/OrderTheory/Posets/PointedPosets.v +++ b/UniMath/OrderTheory/Posets/PointedPosets.v @@ -70,7 +70,7 @@ Definition make_pointed_PartialOrder : pointed_PartialOrder X := RX ,, x ,, p. -Coercion pointed_PartialOrder_to_Partial_order +#[reversible] Coercion pointed_PartialOrder_to_Partial_order {X : hSet} (RX : pointed_PartialOrder X) : PartialOrder X @@ -147,7 +147,7 @@ Definition is_strict_and_monotone : UU := is_monotone RX RY f × f ⊥_{RX} = ⊥_{RY}. -Coercion is_strict_and_monotone_function_to_is_monotone +#[reversible] Coercion is_strict_and_monotone_function_to_is_monotone {X Y : hSet} {RX : pointed_PartialOrder X} {RY : pointed_PartialOrder Y} diff --git a/UniMath/Semantics/EnrichedEffectCalculus/EECModel.v b/UniMath/Semantics/EnrichedEffectCalculus/EECModel.v index db24ad653b..3f4d96898a 100644 --- a/UniMath/Semantics/EnrichedEffectCalculus/EECModel.v +++ b/UniMath/Semantics/EnrichedEffectCalculus/EECModel.v @@ -103,7 +103,7 @@ Definition eec_plus_model × BinCoproducts (pr1 M). -Coercion eec_plus_model_to_eec_model +#[reversible] Coercion eec_plus_model_to_eec_model (E : eec_plus_model) : eec_model := pr1 E. diff --git a/UniMath/Semantics/LinearLogic/LafontCategory.v b/UniMath/Semantics/LinearLogic/LafontCategory.v index 4a95a49fab..9e05d32e85 100644 --- a/UniMath/Semantics/LinearLogic/LafontCategory.v +++ b/UniMath/Semantics/LinearLogic/LafontCategory.v @@ -43,7 +43,7 @@ Definition lafont_category := ∑ (V : sym_mon_closed_cat), is_left_adjoint (underlying_commutative_comonoid V). -Coercion lafont_category_to_sym_mon_closed_cat +#[reversible] Coercion lafont_category_to_sym_mon_closed_cat (V : lafont_category) : sym_mon_closed_cat := pr1 V. diff --git a/UniMath/Semantics/LinearLogic/LinearCategory.v b/UniMath/Semantics/LinearLogic/LinearCategory.v index cdd267bfe8..c2f4abc2bf 100644 --- a/UniMath/Semantics/LinearLogic/LinearCategory.v +++ b/UniMath/Semantics/LinearLogic/LinearCategory.v @@ -54,7 +54,7 @@ Definition make_linear_category_data : linear_category_data := 𝕃 ,, bang ,, δ ,, ε. -Coercion linear_category_data_to_sym_mon_closed_cat +#[reversible] Coercion linear_category_data_to_sym_mon_closed_cat (𝕃 : linear_category_data) : sym_mon_closed_cat := pr1 𝕃. @@ -203,7 +203,7 @@ Definition make_linear_category : linear_category := 𝕃 ,, H. -Coercion linear_category_to_data +#[reversible] Coercion linear_category_to_data (𝕃 : linear_category) : linear_category_data := pr1 𝕃. diff --git a/UniMath/Semantics/LinearLogic/LinearNonLinear.v b/UniMath/Semantics/LinearLogic/LinearNonLinear.v index 94b48ce43d..e5fdd95ed4 100644 --- a/UniMath/Semantics/LinearLogic/LinearNonLinear.v +++ b/UniMath/Semantics/LinearLogic/LinearNonLinear.v @@ -48,7 +48,7 @@ Definition linear_non_linear_model (** 2. Accessors and builders *) -Coercion linear_non_linear_model_to_linear +#[reversible] Coercion linear_non_linear_model_to_linear (𝕃 : linear_non_linear_model) : sym_mon_closed_cat := pr1 𝕃.