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
|
(* An example involving a first-order unification triggering a cyclic constraint *)
Module A.
Notation "{ x : A | P }" := (sigT (fun x:A => P)).
Notation "( x ; y )" := (existT _ x y) : fibration_scope.
Open Scope fibration_scope.
Notation "p @ q" := (eq_trans p q) (at level 20).
Notation "p ^" := (eq_sym p) (at level 3).
Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x)
: P y :=
match p with eq_refl => u end.
Notation "p # x" := (transport _ p x) (right associativity, at level 65, only
parsing).
Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
:= match p with eq_refl => eq_refl end.
Definition apD {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y): p # (f
x) = f y
:= match p with eq_refl => eq_refl end.
Axiom transport_compose
: forall {A B} {x y : A} (P : B -> Type) (f : A -> B) (p : x = y) (z : P (f
x)),
transport (fun x => P (f x)) p z = transport P (ap f p) z.
Delimit Scope morphism_scope with morphism.
Delimit Scope category_scope with category.
Delimit Scope object_scope with object.
Record PreCategory := { object :> Type ; morphism : object -> object -> Type }.
Delimit Scope functor_scope with functor.
Record Functor (C D : PreCategory) :=
{ object_of :> C -> D;
morphism_of : forall s d, morphism C s d -> morphism D (object_of s)
(object_of d) }.
Arguments object_of {C%_category D%_category} f%_functor c%_object : rename, simpl
nomatch.
Arguments morphism_of [C%_category] [D%_category] f%_functor [s%_object d%_object]
m%morphism : rename, simpl nomatch.
Section path_functor.
Variable C : PreCategory.
Variable D : PreCategory.
Local Notation path_functor'_T F G
:= { HO : object_of F = object_of G
| transport (fun GO => forall s d, morphism C s d -> morphism D (GO s)
(GO d))
HO
(morphism_of F)
= morphism_of G }
(only parsing).
Definition path_functor'_sig_inv (F G : Functor C D) : F = G ->
path_functor'_T F G
:= fun H'
=> (ap object_of H';
(transport_compose _ object_of _ _) ^ @ apD (@morphism_of _ _) H').
End path_functor.
End A.
(* A variant of it with more axioms *)
Module B.
Notation "{ x : A | P }" := (sigT (fun x:A => P)).
Notation "( x ; y )" := (existT _ x y).
Notation "p @ q" := (eq_trans p q) (at level 20).
Notation "p ^" := (eq_sym p) (at level 3).
Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y.
Notation "p # x" := (transport _ p x) (right associativity, at level 65, only
parsing).
Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
:= match p with eq_refl => eq_refl end.
Axiom apD : forall {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y), p # (f
x) = f y.
Axiom transport_compose
: forall {A B} {x y : A} (P : B -> Type) (f : A -> B) (p : x = y) (z : P (f
x)),
transport (fun x => P (f x)) p z = transport P (ap f p) z.
Record PreCategory := { object :> Type ; morphism : object -> object -> Type }.
Record Functor (C D : PreCategory) :=
{ object_of :> C -> D;
morphism_of : forall s d, morphism C s d -> morphism D (object_of s)
(object_of d) }.
Arguments object_of {C D} f c : rename, simpl nomatch.
Arguments morphism_of [C] [D] f [s d] m : rename, simpl nomatch.
Section path_functor.
Variable C D : PreCategory.
Local Notation path_functor'_T F G
:= { HO : object_of F = object_of G
| transport (fun GO => forall s d, morphism C s d -> morphism D (GO s)
(GO d))
HO
(morphism_of F)
= morphism_of G }.
Definition path_functor'_sig_inv (F G : Functor C D) : F = G ->
path_functor'_T F G
:= fun H'
=> (ap object_of H';
(transport_compose _ object_of _ _) ^ @ apD (@morphism_of _ _) H').
End path_functor.
End B.
|
