-
Notifications
You must be signed in to change notification settings - Fork 69
/
Setoid.v
77 lines (60 loc) · 2.5 KB
/
Setoid.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
Set Warnings "-notation-overridden".
Require Export Category.Lib.Foundation.
Require Export Coq.Classes.CEquivalence.
Require Export Coq.Classes.CRelationClasses.
Require Export Coq.Classes.CMorphisms.
Generalizable All Variables.
Set Primitive Projections.
Set Universe Polymorphism.
Unset Transparent Obligations.
Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
(at level 200, x binder, y binder, right associativity) :
category_theory_scope.
Notation "'exists' x .. y , p" := (sigT (fun x => .. (sigT (fun y => p)) ..))
(at level 200, x binder, right associativity,
format "'[' 'exists' '/ ' x .. y , '/ ' p ']'") :
category_theory_scope.
Notation "∃ x .. y , P" := (exists x, .. (exists y, P) ..)
(at level 200, x binder, y binder, right associativity) :
category_theory_scope.
Notation "x → y" := (x -> y)
(at level 99, y at level 200, right associativity): category_theory_scope.
Notation "x ↔ y" := (iffT x y)
(at level 95, no associativity) : category_theory_scope.
Notation "¬ x" := (~x)
(at level 75, right associativity) : category_theory_scope.
Notation "x ≠ y" := (x <> y) (at level 70) : category_theory_scope.
Infix "∧" := prod (at level 80, right associativity) : category_theory_scope.
Notation "P ∨ Q" := ({ P } + { Q })
(at level 85, right associativity) : category_theory_scope.
Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..)
(at level 200, x binder, y binder, right associativity) :
category_theory_scope.
Class Setoid A := {
equiv : crelation A;
setoid_equiv :> Equivalence equiv
}.
Notation "f ≈ g" := (equiv f g) (at level 79) : category_theory_scope.
Program Instance setoid_refl `(sa : Setoid A) :
Reflexive equiv.
Obligation 1. apply setoid_equiv. Qed.
Program Instance setoid_sym `(sa : Setoid A) :
Symmetric equiv.
Obligation 1. apply setoid_equiv; auto. Qed.
Program Instance setoid_trans `(sa : Setoid A) :
Transitive equiv.
Obligation 1.
apply setoid_equiv.
destruct sa; simpl in *.
destruct setoid_equiv0.
eapply Equivalence_Transitive; eauto.
Qed.
Delimit Scope signature_scope with signature.
Notation "f ++> g" := (respectful f g)%signature
(right associativity, at level 55) : signature_scope.
Notation "f ==> g" := (respectful f g)%signature
(right associativity, at level 55) : signature_scope.
Notation "f --> g" := (respectful (Basics.flip f) g)%signature
(right associativity, at level 55) : signature_scope.
Arguments Proper {A}%type R%signature m.
Arguments respectful {A B}%type (R R')%signature _ _.