-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathDuals.v
131 lines (102 loc) · 4.94 KB
/
Duals.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
Require Import JMeq Eqdep.
Require Export SpecializedCategory CategoryIsomorphisms Functor ProductCategory NaturalTransformation.
Require Import Common Notations FEqualDep.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Universe Polymorphism.
Local Infix "==" := JMeq.
Local Open Scope category_scope.
Section OppositeCategory.
Definition OppositeCategory `(C : @SpecializedCategory objC) : @SpecializedCategory objC
:= @Build_SpecializedCategory' objC
(fun s d => Morphism C d s)
(Identity (C := C))
(fun _ _ _ m1 m2 => Compose m2 m1)
(fun _ _ _ _ _ _ _ => @Associativity_sym _ _ _ _ _ _ _ _ _)
(fun _ _ _ _ _ _ _ => @Associativity _ _ _ _ _ _ _ _ _)
(fun _ _ => @RightIdentity _ _ _ _)
(fun _ _ => @LeftIdentity _ _ _ _).
End OppositeCategory.
(*Notation "C ᵒᵖ" := (OppositeCategory C) : category_scope.*)
Section DualCategories.
Context `(C : @SpecializedCategory objC).
Context `(D : @SpecializedCategory objD).
Lemma op_op_id : OppositeCategory (OppositeCategory C) = C.
clear D objD.
unfold OppositeCategory; simpl.
repeat change (fun a => ?f a) with f.
destruct C; intros; simpl; reflexivity.
Qed.
Lemma op_distribute_prod : OppositeCategory (C * D) = (OppositeCategory C) * (OppositeCategory D).
spcat_eq.
Qed.
End DualCategories.
Hint Rewrite @op_op_id @op_distribute_prod : category.
Section DualObjects.
Context `(C : @SpecializedCategory objC).
Definition terminal_opposite_initial (o : C) : IsTerminalObject o -> IsInitialObject (C := OppositeCategory C) o
:= fun H o' => H o'.
Definition initial_opposite_terminal (o : C) : IsInitialObject o -> IsTerminalObject (C := OppositeCategory C) o
:= fun H o' => H o'.
Definition terminal_to_opposite_initial : TerminalObject C -> InitialObject (OppositeCategory C)
:= Eval cbv beta iota zeta delta [terminal_opposite_initial TerminalObject_IsTerminalObject IsInitialObject_InitialObject proj1_sig proj2_sig] in
fun x => terminal_opposite_initial x.
Definition initial_to_opposite_terminal : InitialObject C -> TerminalObject (OppositeCategory C)
:= Eval cbv beta iota zeta delta [initial_opposite_terminal IsTerminalObject_TerminalObject InitialObject_IsInitialObject proj1_sig proj2_sig] in
fun x => initial_opposite_terminal x.
End DualObjects.
Section OppositeFunctor.
Context `(C : @SpecializedCategory objC).
Context `(D : @SpecializedCategory objD).
Variable F : SpecializedFunctor C D.
Let COp := OppositeCategory C.
Let DOp := OppositeCategory D.
Definition OppositeFunctor : SpecializedFunctor COp DOp.
refine (Build_SpecializedFunctor COp DOp
(fun c : COp => F c : DOp)
(fun (s d : COp) (m : C.(Morphism) d s) => MorphismOf F (s := d) (d := s) m)
(fun d' d s m1 m2 => FCompositionOf F s d d' m2 m1)
(FIdentityOf F)
).
Defined.
End OppositeFunctor.
(*Notation "C ᵒᵖ" := (OppositeFunctor C) : functor_scope.*)
Section OppositeFunctor_Id.
Context `(C : @SpecializedCategory objC).
Context `(D : @SpecializedCategory objD).
Variable F : SpecializedFunctor C D.
Lemma op_op_functor_id : OppositeFunctor (OppositeFunctor F) == F.
functor_eq; autorewrite with category; trivial.
Qed.
End OppositeFunctor_Id.
(* not terribly useful, given that this would make [autorewrite with core] give "Anomaly: Uncaught exception Failure("nth"). Please report." *)
(*Hint Rewrite op_op_functor_id.*)
Section OppositeNaturalTransformation.
Context `(C : @SpecializedCategory objC).
Context `(D : @SpecializedCategory objD).
Variables F G : SpecializedFunctor C D.
Variable T : SpecializedNaturalTransformation F G.
Let COp := OppositeCategory C.
Let DOp := OppositeCategory D.
Let FOp := OppositeFunctor F.
Let GOp := OppositeFunctor G.
Definition OppositeNaturalTransformation : SpecializedNaturalTransformation GOp FOp.
refine (Build_SpecializedNaturalTransformation GOp FOp
(fun c : COp => T.(ComponentsOf) c : DOp.(Morphism) (GOp c) (FOp c))
(fun s d m => eq_sym (Commutes T d s m))
).
Defined.
End OppositeNaturalTransformation.
(*Notation "C ᵒᵖ" := (OppositeNaturalTransformation C) : natural_transformation_scope.*)
Section OppositeNaturalTransformation_Id.
Context `(C : @SpecializedCategory objC).
Context `(D : @SpecializedCategory objD).
Variables F G : SpecializedFunctor C D.
Variable T : SpecializedNaturalTransformation F G.
Lemma op_op_nt_id : OppositeNaturalTransformation (OppositeNaturalTransformation T) == T.
nt_eq; intros; try functor_eq; autorewrite with category; subst; trivial.
Qed.
End OppositeNaturalTransformation_Id.
(* not terribly useful, given that this would make [autorewrite with core] give "Anomaly: Uncaught exception Failure("nth"). Please report." *)
(*Hint Rewrite op_op_nt_id.*)