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
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
|
Require
MathClasses.misc.JMrelation.
Require Import
MathClasses.interfaces.abstract_algebra MathClasses.interfaces.functors MathClasses.theory.categories.
Record Object := object
{ obj:> Type
; Arrows_inst: Arrows obj
; Equiv_inst: ∀ x y: obj, Equiv (x ⟶ y)
; CatId_inst: CatId obj
; CatComp_inst: CatComp obj
; Category_inst: Category obj }.
Arguments object _ {Arrows_inst Equiv_inst CatId_inst CatComp_inst Category_inst}.
#[global]
Existing Instance Arrows_inst.
#[global]
Existing Instance Equiv_inst.
#[global]
Existing Instance CatId_inst.
#[global]
Existing Instance CatComp_inst.
#[global]
Existing Instance Category_inst.
Record Arrow (x y: Object): Type := arrow
{ map_obj:> obj x → obj y
; Fmap_inst: Fmap map_obj
; Functor_inst: Functor map_obj _ }.
Arguments arrow {x y} _ _ _.
Arguments map_obj {x y} _ _.
#[global]
Existing Instance Fmap_inst.
#[global]
Existing Instance Functor_inst.
#[global]
Instance: Arrows Object := Arrow.
(* Hint Extern 4 (Arrows Object) => exact Arrow: typeclass_instances. *)
Section contents.
Section more_arrows.
Context (x y: Object).
Global Instance e: Equiv (x ⟶ y) := λ a b,
(∀ v, a v ≡ b v) ∧
(∀ `(f: v ⟶ w), JMrelation.R (=) (fmap a f) _ (=) (fmap b f)).
Instance e_refl: Reflexive e.
Proof.
intro a. unfold e. intuition.
apply JMrelation.reflexive, _.
Qed.
Instance e_sym: Symmetric e.
Proof with intuition.
unfold e. intros ?? [P Q]...
apply JMrelation.symmetric...
Qed.
Instance e_trans: Transitive e.
Proof with intuition.
unfold e. intros a b c [P Q] [R S]...
transitivity (b v)...
apply JMrelation.transitive with _ (=) (fmap b f)...
Qed.
Global Instance: Setoid (x ⟶ y).
Proof. split; apply _. Qed.
End more_arrows.
Global Instance: CatId Object := λ _, arrow id _ _.
Global Program Instance: CatComp Object := λ _ _ _ x y, arrow (x ∘ y) _ _.
Global Instance: ∀ x y z: Object, Proper ((=) ==> (=) ==> (=)) ((◎): (y ⟶ z) → (x ⟶ y) → (x ⟶ z)).
Proof with intuition; try apply _.
unfold equiv, e.
intros x y z a b [P Q] c d [R S].
split; intros.
change (a (c v) ≡ b (d v)). congruence.
change (JMrelation.R (=) (fmap a (fmap c f)) _ (=) (fmap b (fmap d f))).
apply JMrelation.transitive with _ (=) (fmap a (fmap d f))...
specialize (S _ _ f). revert S.
generalize (fmap c f) (fmap d f).
repeat rewrite R.
intros. apply JMrelation.relate.
rewrite (JMrelation.unJM _ _ _ _ _ S)... (* <- uses K *)
Qed.
Global Instance: Category Object.
Proof. repeat (split; try apply _); intuition; apply reflexivity. Qed.
End contents.
|
