-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathCommaCategory.v
153 lines (127 loc) · 6.47 KB
/
CommaCategory.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
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
Require Import ProofIrrelevance.
Require Export Category SpecializedCategory Functor ProductCategory.
Require Import Common Notations InitialTerminalCategory SpecializedCommaCategory DefinitionSimplification.
Set Implicit Arguments.
Set Asymmetric Patterns.
Set Universe Polymorphism.
Local Open Scope category_scope.
Local Ltac fold_functor := idtac. (*
change CObject with (fun C => @Object (CObject C) C) in *;
change (@SpecializedFunctor) with (fun objC (C : @SpecializedCategory objC) objD (D : @SpecializedCategory objD) => @Functor C D) in *. *)
Section CommaCategory.
(* [Definition]s are not sort-polymorphic, and it's too slow to not use
[Definition]s, so we might as well use [Category]s rather than [SpecializedCategory]s. *)
Variable A : Category.
Variable B : Category.
Variable C : Category.
Variable S : Functor A C.
Variable T : Functor B C.
(** Quoting Wikipedia:
Suppose that [A], [B], and [C] are categories, and [S] and [T]
are functors
[S : A -> C <- B : T]
We can form the comma category [(S ↓ T)] as follows:
(o) The objects are all triples [(α, β, f)] with [α] an object in
[A], [β] an object in [B], and [f : S α -> T β] a morphism in
[C].
(o) The morphisms from [(α, β, f)] to [(α', β', f')] are all
pairs [(g, h)] where [g : α -> α'] and [h : β -> β'] are
morphisms in [A] and [B] respectively, such that the
following diagram commutes:
[[
S g
S α -----> S α'
| |
f | | f'
| |
V V
T β -----> T β'
T h
]]
Morphisms are composed by taking [(g, h) ○ (g', h')] to be
[(g ○ g', h ○ h')], whenever the latter expression is defined.
The identity morphism on an object [(α, β, f)] is [(Identity α, Identity β)].
*)
(* By definining all the parts separately, we can make the [Prop]
Parts of the definition opaque via [abstract]. This speeds things
up significantly. We unfold the definitions at the very end with
[Eval]. *)
(* stupid lack of sort-polymorphism in definitions... *)
Let CommaCategory_Object' := Eval hnf in CommaSpecializedCategory_ObjectT S T.
Let CommaCategory_Object'' : Type.
simpl_definition_by_tac_and_exact CommaCategory_Object' ltac:(simpl in *; fold_functor).
Defined.
Definition CommaCategory_Object := Eval cbv beta delta [CommaCategory_Object''] in CommaCategory_Object''.
Let CommaCategory_Morphism' (XG X'G' : CommaCategory_Object) := Eval hnf in CommaSpecializedCategory_MorphismT (S := S) (T := T) XG X'G'.
Let CommaCategory_Morphism'' (XG X'G' : CommaCategory_Object) : Type.
simpl_definition_by_tac_and_exact (CommaCategory_Morphism' XG X'G') ltac:(subst_body; cbv beta in *; fold_functor; cbv beta in *).
Defined.
Definition CommaCategory_Morphism (XG X'G' : CommaCategory_Object) := Eval hnf in CommaCategory_Morphism'' XG X'G'.
Let CommaCategory_Compose' s d d' Fα F'α'
:= Eval hnf in CommaSpecializedCategory_Compose (S := S) (T := T) (s := s) (d := d) (d' := d') Fα F'α'.
Let CommaCategory_Compose'' s d d' (Fα : CommaCategory_Morphism d d') (F'α' : CommaCategory_Morphism s d) :
CommaCategory_Morphism s d'.
simpl_definition_by_tac_and_exact (@CommaCategory_Compose' s d d' Fα F'α') ltac:(subst_body; cbv beta in *; fold_functor; cbv beta in *).
Defined.
Definition CommaCategory_Compose s d d' (Fα : CommaCategory_Morphism d d') (F'α' : CommaCategory_Morphism s d) :
CommaCategory_Morphism s d'
:= Eval hnf in @CommaCategory_Compose'' s d d' Fα F'α'.
Let CommaCategory_Identity' o := Eval hnf in CommaSpecializedCategory_Identity (S := S) (T := T) o.
Let CommaCategory_Identity'' (o : CommaCategory_Object) : CommaCategory_Morphism o o.
simpl_definition_by_tac_and_exact (@CommaCategory_Identity' o) ltac:(subst_body; cbv beta in *; fold_functor; cbv beta in *).
Defined.
Definition CommaCategory_Identity (o : CommaCategory_Object) : CommaCategory_Morphism o o
:= Eval hnf in @CommaCategory_Identity'' o.
Global Arguments CommaCategory_Compose _ _ _ _ _ /.
Global Arguments CommaCategory_Identity _ /.
Lemma CommaCategory_Associativity o1 o2 o3 o4 (m1 : CommaCategory_Morphism o1 o2) (m2 : CommaCategory_Morphism o2 o3) (m3 : CommaCategory_Morphism o3 o4) :
CommaCategory_Compose (CommaCategory_Compose m3 m2) m1 = CommaCategory_Compose m3 (CommaCategory_Compose m2 m1).
abstract apply (CommaSpecializedCategory_Associativity (S := S) (T := T) m1 m2 m3).
Qed.
Lemma CommaCategory_LeftIdentity (a b : CommaCategory_Object) (f : CommaCategory_Morphism a b) :
CommaCategory_Compose (CommaCategory_Identity b) f = f.
Proof.
abstract apply (CommaSpecializedCategory_LeftIdentity (S := S) (T := T) f).
Qed.
Lemma CommaCategory_RightIdentity (a b : CommaCategory_Object) (f : CommaCategory_Morphism a b) :
CommaCategory_Compose f (CommaCategory_Identity a) = f.
Proof.
abstract apply (CommaSpecializedCategory_RightIdentity (S := S) (T := T) f).
Qed.
Definition CommaCategory : Category.
refine (@Build_SpecializedCategory CommaCategory_Object CommaCategory_Morphism
CommaCategory_Identity
CommaCategory_Compose
_ _ _
);
subst_body;
abstract (apply CommaCategory_Associativity || apply CommaCategory_LeftIdentity || apply CommaCategory_RightIdentity).
Defined.
End CommaCategory.
Hint Unfold CommaCategory_Compose CommaCategory_Identity CommaCategory_Morphism CommaCategory_Object : category.
Arguments CommaCategory [A B C] S T.
Local Notation "S ↓ T" := (CommaCategory S T).
Section SliceCategory.
Variable A : Category.
Variable C : Category.
Variable a : C.
Variable S : Functor A C.
Let B := TerminalCategory.
Definition SliceCategory_Functor : Functor B C.
refine {| ObjectOf := (fun _ => a);
MorphismOf := (fun _ _ _ => Identity a)
|}; abstract (intros; auto with morphism).
Defined.
Definition SliceCategory := CommaCategory S SliceCategory_Functor.
Definition CosliceCategory := CommaCategory SliceCategory_Functor S.
End SliceCategory.
Section SliceCategoryOver.
Variable C : Category.
Variable a : C.
Definition SliceCategoryOver := SliceCategory a (IdentityFunctor C).
Definition CosliceCategoryOver := CosliceCategory a (IdentityFunctor C).
End SliceCategoryOver.
Section ArrowCategory.
Variable C : Category.
Definition ArrowCategory := CommaCategory (IdentityFunctor C) (IdentityFunctor C).
End ArrowCategory.