Skip to content

Commit 6e6cda4

Browse files
committed
1 parent c67b016 commit 6e6cda4

File tree

6 files changed

+16
-8
lines changed

6 files changed

+16
-8
lines changed

Lib/Setoid.v

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -43,8 +43,9 @@ Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..)
4343

4444
Class Setoid A := {
4545
equiv : crelation A;
46-
setoid_equiv :> Equivalence equiv
46+
setoid_equiv : Equivalence equiv
4747
}.
48+
#[export] Existing Instance setoid_equiv.
4849

4950
Notation "f ≈ g" := (equiv f g) (at level 79) : category_theory_scope.
5051

Structure/Cartesian.v

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,12 +24,13 @@ Class Cartesian:= {
2424
exl {x y} : x × y ~> x;
2525
exr {x y} : x × y ~> y;
2626

27-
fork_respects :> ∀ x y z,
27+
fork_respects : ∀ x y z,
2828
Proper (equiv ==> equiv ==> equiv) (@fork x y z);
2929

3030
ump_products {x y z} (f : x ~> y) (g : x ~> z) (h : x ~> y × z) :
3131
h ≈ fork f g ↔ (exl ∘ h ≈ f) * (exr ∘ h ≈ g)
3232
}.
33+
#[export] Existing Instance fork_respects.
3334

3435
Infix "×" := product_obj (at level 40, left associativity) : object_scope.
3536
Infix "△" := fork (at level 28) : morphism_scope.

Structure/Monoidal/Cartesian.v

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -31,14 +31,16 @@ Context {C : Category}.
3131
augmentations must in fact be cartesian monoidal." *)
3232

3333
Class CartesianMonoidal `{@Monoidal C} := {
34-
is_semicartesian :> @SemicartesianMonoidal C _;
35-
is_relevance :> @RelevantMonoidal C _;
34+
is_semicartesian : @SemicartesianMonoidal C _;
35+
is_relevance : @RelevantMonoidal C _;
3636

3737
proj_left_diagonal {x} : proj_left ∘ diagonal ≈ id[x];
3838
proj_right_diagonal {x} : proj_right ∘ diagonal ≈ id[x];
3939

4040
unit_left_twist {x} : unit_left ∘ @twist _ _ _ x I ≈ unit_right;
4141
unit_right_twist {x} : unit_right ∘ @twist _ _ _ I x ≈ unit_left
4242
}.
43+
#[export] Existing Instance is_semicartesian.
44+
#[export] Existing Instance is_relevance.
4345

4446
End CartesianMonoidal.

Structure/Monoidal/Relevant.v

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ Section RelevantMonoidal.
1919
Context {C : Category}.
2020

2121
Class RelevantMonoidal `{@Monoidal C} := {
22-
is_symmetric :> SymmetricMonoidal;
22+
is_symmetric : SymmetricMonoidal;
2323

2424
diagonal {x} : x ~> x ⨂ x;
2525
diagonal_natural : natural (@diagonal);
@@ -43,6 +43,7 @@ Class RelevantMonoidal `{@Monoidal C} := {
4343
diagonal_twist2 {x y} :
4444
@diagonal (x ⨂ y) ≈ twist2 ∘ diagonal ⨂ diagonal
4545
}.
46+
#[export] Existing Instance is_symmetric.
4647

4748
Lemma twist2_natural `{@Monoidal C} `{@RelevantMonoidal _} :
4849
natural (@twist2 _ _).

Theory/Category.v

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -40,13 +40,13 @@ Class Category := {
4040

4141
uhom := Type : Type;
4242
hom : obj -> obj -> uhom where "a ~> b" := (hom a b);
43-
homset :> ∀ X Y, Setoid (X ~> Y);
43+
homset : ∀ X Y, Setoid (X ~> Y);
4444

4545
id {x} : x ~> x;
4646
compose {x y z} (f: y ~> z) (g : x ~> y) : x ~> z
4747
where "f ∘ g" := (compose f g);
4848

49-
compose_respects x y z :>
49+
compose_respects x y z :
5050
Proper (equiv ==> equiv ==> equiv) (@compose x y z);
5151

5252
dom {x y} (f: x ~> y) := x;
@@ -60,6 +60,8 @@ Class Category := {
6060
comp_assoc_sym {x y z w} (f : z ~> w) (g : y ~> z) (h : x ~> y) :
6161
(f ∘ g) ∘ h ≈ f ∘ (g ∘ h)
6262
}.
63+
#[export] Existing Instance homset.
64+
#[export] Existing Instance compose_respects.
6365

6466
Declare Scope category_scope.
6567
Declare Scope object_scope.

Theory/Functor.v

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,12 +21,13 @@ Class Functor {C D : Category} := {
2121
fobj : C -> D;
2222
fmap {x y : C} (f : x ~> y) : fobj x ~> fobj y;
2323

24-
fmap_respects :> ∀ x y, Proper (equiv ==> equiv) (@fmap x y);
24+
fmap_respects : ∀ x y, Proper (equiv ==> equiv) (@fmap x y);
2525

2626
fmap_id {x : C} : fmap (@id C x) ≈ id;
2727
fmap_comp {x y z : C} (f : y ~> z) (g : x ~> y) :
2828
fmap (f ∘ g) ≈ fmap f ∘ fmap g
2929
}.
30+
#[export] Existing Instance fmap_respects.
3031

3132
Declare Scope functor_scope.
3233
Declare Scope functor_type_scope.

0 commit comments

Comments
 (0)