Skip to content

Commit

Permalink
Adapt to coq/coq#18590
Browse files Browse the repository at this point in the history
  • Loading branch information
@proux01
proux01 committed Jan 31, 2024
1 parent dda1049 commit 6216ca4
Show file tree
Hide file tree
Showing 2 changed files with 84 additions and 43 deletions.
106 changes: 70 additions & 36 deletions theories/Basics/CategoryTheory.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,12 +37,16 @@ Class CatAssoc : Prop :=
(f >>> g) >>> h ⩯ f >>> (g >>> h).

Class Category : Prop := {
category_cat_id_l :> CatIdL;
category_cat_id_r :> CatIdR;
category_cat_assoc :> CatAssoc;
category_proper_cat :> forall a b c,
category_cat_id_l : CatIdL;
category_cat_id_r : CatIdR;
category_cat_assoc : CatAssoc;
category_proper_cat : forall a b c,
@Proper (C a b -> C b c -> C a c) (eq2 ==> eq2 ==> eq2) cat;
}.
#[global] Existing Instance category_cat_id_l.
#[global] Existing Instance category_cat_id_r.
#[global] Existing Instance category_cat_assoc.
#[global] Existing Instance category_proper_cat.

(** *** Initial object *)

Expand Down Expand Up @@ -154,9 +158,11 @@ Section DaggerLaws.
Local Existing Instance Id_Op.
Local Existing Instance Cat_Op.
Class DaggerLaws : Prop := {
dagger_involution :> DaggerInvolution ;
dagger_functor :> Functor (op C) C id (@dagger obj C _)
dagger_involution : DaggerInvolution ;
dagger_functor : Functor (op C) C id (@dagger obj C _)
}.
#[global] Existing Instance dagger_involution.
#[global] Existing Instance dagger_functor.

End DaggerLaws.

Expand All @@ -183,11 +189,14 @@ Class BimapCat : Prop :=
bimap f1 f2 >>> bimap g1 g2 ⩯ bimap (f1 >>> g1) (f2 >>> g2).

Class Bifunctor : Prop := {
bifunctor_bimap_id :> BimapId;
bifunctor_bimap_cat :> BimapCat;
bifunctor_proper_bimap :> forall a b c d,
bifunctor_bimap_id : BimapId;
bifunctor_bimap_cat : BimapCat;
bifunctor_proper_bimap : forall a b c d,
@Proper (C a c -> C b d -> C _ _) (eq2 ==> eq2 ==> eq2) bimap;
}.
#[global] Existing Instance bifunctor_bimap_id.
#[global] Existing Instance bifunctor_bimap_cat.
#[global] Existing Instance bifunctor_proper_bimap.

End BifunctorLaws.

Expand Down Expand Up @@ -224,12 +233,16 @@ Class CaseUniversal : Prop :=
fg ⩯ case_ f g.

Class Coproduct : Prop := {
coproduct_case_inl :> CaseInl;
coproduct_case_inr :> CaseInr;
coproduct_case_universal :> CaseUniversal;
coproduct_proper_case :> forall a b c,
coproduct_case_inl : CaseInl;
coproduct_case_inr : CaseInr;
coproduct_case_universal : CaseUniversal;
coproduct_proper_case : forall a b c,
@Proper (C a c -> C b c -> C _ c) (eq2 ==> eq2 ==> eq2) case_
}.
#[global] Existing Instance coproduct_case_inl.
#[global] Existing Instance coproduct_case_inr.
#[global] Existing Instance coproduct_case_universal.
#[global] Existing Instance coproduct_proper_case.

End CoproductLaws.

Expand Down Expand Up @@ -270,12 +283,16 @@ Class PairUniversal : Prop :=
fg ⩯ pair_ f g.

Class Product : Prop := {
product_pair_fst :> PairFst;
product_pair_snd :> PairSnd;
product_pair_universal :> PairUniversal;
product_proper_pair :> forall a b c,
product_pair_fst : PairFst;
product_pair_snd : PairSnd;
product_pair_universal : PairUniversal;
product_proper_pair : forall a b c,
@Proper (C c a -> C c b -> C c _) (eq2 ==> eq2 ==> eq2) pair_
}.
#[global] Existing Instance product_pair_fst.
#[global] Existing Instance product_pair_snd.
#[global] Existing Instance product_pair_universal.
#[global] Existing Instance product_proper_pair.

End ProductLaws.

Expand Down Expand Up @@ -306,13 +323,17 @@ Class CurryApply : Prop :=
f ⩯ ((@bimap obj C PROD _ _ _ _ _ (curry_ f) (id_ a)) >>> apply_).

Class CartesianClosed : Prop := {
cartesian_terminal :> TerminalObject _ ONE;
cartesian_product :> Product _ PROD;
cartesian_curry_apply :> CurryApply;
cartesian_proper_curry_ :> forall a b c,
@Proper (C (PROD c a) b -> C c (EXP a b)) (eq2 ==> eq2) curry_
cartesian_terminal : TerminalObject _ ONE;
cartesian_product : Product _ PROD;
cartesian_curry_apply : CurryApply;
cartesian_proper_curry_ : forall a b c,
@Proper (C (PROD c a) b -> C c (EXP a b)) (eq2 ==> eq2) curry_
}.

#[global] Existing Instance cartesian_terminal.
#[global] Existing Instance cartesian_product.
#[global] Existing Instance cartesian_curry_apply.
#[global] Existing Instance cartesian_proper_curry_.

End CartesianClosureLaws.

Arguments curry_apply {obj C Eq2_C Id_C Cat_C PROD Pair_C Fst_C Snd_C EXP Apply_C Curry_C} _ [a b c] f.
Expand Down Expand Up @@ -420,15 +441,23 @@ Class AssocRAssocR : Prop :=
⩯ assoc_r >>> assoc_r.

Class Monoidal : Prop := {
monoidal_bifunctor :> Bifunctor C bif;
monoidal_assoc_iso :> AssocIso;
monoidal_unit_l_iso :> UnitLIso;
monoidal_unit_r_iso :> UnitRIso;
monoidal_unit_l_natural :> UnitLNatural;
monoidal_unit_l'_natural :> UnitL'Natural;
monoidal_assoc_r_unit :> AssocRUnit;
monoidal_assoc_r_assoc_r :> AssocRAssocR;
monoidal_bifunctor : Bifunctor C bif;
monoidal_assoc_iso : AssocIso;
monoidal_unit_l_iso : UnitLIso;
monoidal_unit_r_iso : UnitRIso;
monoidal_unit_l_natural : UnitLNatural;
monoidal_unit_l'_natural : UnitL'Natural;
monoidal_assoc_r_unit : AssocRUnit;
monoidal_assoc_r_assoc_r : AssocRAssocR;
}.
#[global] Existing Instance monoidal_bifunctor.
#[global] Existing Instance monoidal_assoc_iso.
#[global] Existing Instance monoidal_unit_l_iso.
#[global] Existing Instance monoidal_unit_r_iso.
#[global] Existing Instance monoidal_unit_l_natural.
#[global] Existing Instance monoidal_unit_l'_natural.
#[global] Existing Instance monoidal_assoc_r_unit.
#[global] Existing Instance monoidal_assoc_r_assoc_r.

(** The [assoc_l] variants can be derived by symmetry,
because [assoc_l] is the inverse of [assoc_r]. *)
Expand Down Expand Up @@ -556,13 +585,18 @@ Class IterCodiagonal : Prop :=
(* TODO: also define uniformity, requires a "purity" assumption. *)

Class Iterative : Prop :=
{ iterative_unfold :> IterUnfold
; iterative_natural :> IterNatural
; iterative_dinatural :> IterDinatural
; iterative_codiagonal :> IterCodiagonal
{ iterative_unfold : IterUnfold
; iterative_natural : IterNatural
; iterative_dinatural : IterDinatural
; iterative_codiagonal : IterCodiagonal
; iterative_proper_iter
:> forall a b, @Proper (C a (bif a b) -> C a b) (eq2 ==> eq2) iter
: forall a b, @Proper (C a (bif a b) -> C a b) (eq2 ==> eq2) iter
}.
#[global] Existing Instance iterative_unfold.
#[global] Existing Instance iterative_natural.
#[global] Existing Instance iterative_dinatural.
#[global] Existing Instance iterative_codiagonal.
#[global] Existing Instance iterative_proper_iter.

(** Also called Bekic identity *)
Definition IterPairing : Prop :=
Expand Down
21 changes: 14 additions & 7 deletions theories/Basics/HeterogeneousRelations.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -118,22 +118,29 @@ Class TransitiveH {A: Type} (R : relationH A A) : Prop :=

Class PER {A : Type} (R : relationH A A) : Type :=
{
per_symm :> SymmetricH R;
per_trans :> TransitiveH R
per_symm : SymmetricH R;
per_trans : TransitiveH R
}.
#[global] Existing Instance per_symm.
#[global] Existing Instance per_trans.

Class Preorder {A : Type} (R : relationH A A) : Type :=
{
pre_refl :> ReflexiveH R;
pre_trans :> TransitiveH R
pre_refl : ReflexiveH R;
pre_trans : TransitiveH R
}.
#[global] Existing Instance pre_refl.
#[global] Existing Instance pre_trans.

Class EquivalenceH {A : Type} (R : relationH A A) : Type :=
{
equiv_refl :> ReflexiveH R;
equiv_symm :> SymmetricH R;
equiv_trans :> TransitiveH R
equiv_refl : ReflexiveH R;
equiv_symm : SymmetricH R;
equiv_trans : TransitiveH R
}.
#[global] Existing Instance equiv_refl.
#[global] Existing Instance equiv_symm.
#[global] Existing Instance equiv_trans.

#[global]
Instance relationH_reflexive : forall (A:Type), ReflexiveH (@eq A).
Expand Down

0 comments on commit 6216ca4

Please sign in to comment.