Skip to content

Commit 7b039fc

Browse files
andreaslynandreaslyn
committed
Start doc
1 parent 4ba5866 commit 7b039fc

9 files changed

+110
-47
lines changed

‎interfaces/ua_algebra.v‎

Lines changed: 98 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,8 @@
1+
(** This file defines what an [Algebra] is and provides some
2+
elementary results. *)
3+
14
Require Export
5+
Coq.Unicode.Utf8
26
HoTTClasses.implementations.ne_list
37
HoTTClasses.implementations.family_prod.
48

@@ -25,69 +29,128 @@ Open Scope Algebra_scope.
2529

2630
Local Notation SymbolType_internal := @ne_list.
2731

28-
Record Signature : Type := Build
32+
(** A [Signature] is used to characterise [Algebra]s. It consists of
33+
- A type of [Sort]s, which represent the "objects" (types) an
34+
algebra for the signature must provide.
35+
- A type of Function [Symbol]s, which represent operations an
36+
algebra for the signature must provide.
37+
- For each symbol [u:Symbol], a [SymbolType] specifying the
38+
required type of the operation corresponding to [u] provided by
39+
the algebra for the signature. *)
40+
41+
Record Signature : Type := BuildSignature
2942
{ Sort : Type
3043
; Symbol : Type
3144
; symbol_types : Symbol → SymbolType_internal Sort }.
3245

46+
(** Notice we have this implicit coercion allowing us to use a
47+
signature [σ:Signature] as a map [Symbol σ → SymbolType σ]
48+
(see [SymbolType] below). *)
49+
3350
Global Coercion symbol_types : Signature >-> Funclass.
3451

35-
Definition BuildSingleSortedSignature {Op : Type} (arities : Op → nat)
52+
(** A single sorted [Signature] is a singuture with [Sort = Unit].
53+
Then it suffices to provide an arity for each Function [Symbol]. *)
54+
55+
Definition BuildSingleSortedSignature {sym : Type} (arities : sym → nat)
3656
: Signature
37-
:= Build Unit Op (ne_list.replicate_Sn tt ∘ arities).
57+
:= BuildSignature Unit sym (ne_list.replicate_Sn tt ∘ arities).
58+
59+
(** Let [σ:Signature]. For each symbol [u : Symbol σ], [σ u] is
60+
associates [u] to a [SymbolType σ]. This represents the required
61+
type of the algebra operation corresponding to [u]. *)
62+
63+
Definition SymbolType (σ : Signature) : Type
64+
:= SymbolType_internal (Sort σ).
65+
66+
(** For [s : SymbolType σ], [cod_symboltype σ] is the codomain of the
67+
symbol type [s]. *)
68+
69+
Definition cod_symboltype {σ} : SymbolType σ → Sort σ
70+
:= ne_list.last.
3871

39-
Definition SymbolType (σ : Signature) : Type := SymbolType_internal (Sort σ).
72+
(** For [s : SymbolType σ], [cod_symboltype σ] is the domain of the
73+
symbol type [s]. *)
4074

41-
Definition cod_symboltype {σ} : SymbolType σ → Sort σ := ne_list.last.
75+
Definition dom_symboltype {σ} : SymbolType σ → list (Sort σ)
76+
:= ne_list.front.
4277

43-
Definition dom_symboltype {σ} : SymbolType σ → list (Sort σ) := ne_list.front.
78+
(** For [s : SymbolType σ], [cod_symboltype σ] is the arity of the
79+
symbol type [s]. That is the number [n:nat] of arguments of the
80+
[SymbolType σ]. *)
4481

45-
Definition arity_symboltype {σ} : SymbolType σ → nat := length ∘ dom_symboltype.
82+
Definition arity_symboltype {σ} : SymbolType σ → nat
83+
:= length ∘ dom_symboltype.
84+
85+
(** An [Algebra] must provide a family of [Carriers σ] indexed by
86+
[Sort σ]. These carriers are the "objects" (types) of the algebra. *)
87+
88+
(* [Carriers] is a notation because it will be used for an implicit
89+
coercion [Algebra >-> Funclass] below. *)
4690

4791
Notation Carriers := (λ (σ : Signature), Sort σ → Type).
4892

49-
Fixpoint Operation {σ : Signature} (A : Carriers σ) (u : SymbolType σ) : Type
50-
:= match u with
93+
(** The function [Operation] maps a family of carriers [A : Carriers σ]
94+
and [w : SymbolType σ] to the corresponding function type. For
95+
example
96+
<<
97+
Operation A [:s1; s2; r:] = A s1 → A s2 → A r
98+
>> *)
99+
100+
Fixpoint Operation {σ : Signature} (A : Carriers σ) (w : SymbolType σ)
101+
: Type
102+
:= match w with
51103
| [:s:] => A s
52-
| s ::: u' => A s → Operation A u'
104+
| s ::: w' => A s → Operation A w'
53105
end.
54106

55-
Global Instance trunc_operation `{Funext} {σ : Signature} (A : Carriers σ)
56-
{n} `{!∀ s, IsTrunc n (A s)} (w : SymbolType σ)
57-
: IsTrunc n (Operation A w).
107+
Global Instance trunc_operation `{Funext} {σ : Signature}
108+
(A : Carriers σ) {n} `{!∀ s, IsTrunc n (A s)} (w : SymbolType σ)
109+
: IsTrunc n (Operation A w).
58110
Proof.
59111
induction w; apply (istrunc_trunctype_type (BuildTruncType n _)).
60112
Defined.
61113

62-
(** Uncurry of [Operation], such that
63-
64-
[ap_operation f (x1,x2,...,xn) = f x1 x2 ... xn]. *)
114+
(** Uncurry of an [Operation A w], such that
115+
<<
116+
ap_operation f (x1,x2,...,xn) = f x1 x2 ... xn
117+
>> *)
65118

66119
Fixpoint ap_operation {σ} {A : Carriers σ} {w : SymbolType σ}
67-
: Operation A w → FamilyProd A (dom_symboltype w) → A (cod_symboltype w)
120+
: Operation A w →
121+
FamilyProd A (dom_symboltype w) →
122+
A (cod_symboltype w)
68123
:= match w with
69124
| [:s:] => λ f _, f
70125
| s ::: w' => λ f '(x, l), ap_operation (f x) l
71126
end.
72127

73-
(** Funext for uncurried [Operation]s. If
128+
(** Funext for uncurried [Operation A w]. If
129+
<<
130+
ap_operation f (x1,x2,...,xn) = ap_operation g (x1,x2,...,xn)
131+
>>
132+
for all [(x1,x2,...,xn) : A s1 * A s2 * ... * A sn], then [f = g]. *)
74133

75-
[ap_operation f (x1,x2,...,xn) = ap_operation g (x1,x2,...,xn)],
76-
77-
for all [(x1,x2,...,xn) : A s1 * A s2 * ... A sn], then [f = g].
78-
*)
79-
80-
Fixpoint path_forall_ap_operation `{Funext} {σ} {A : Carriers σ} {w : SymbolType σ}
134+
Fixpoint path_forall_ap_operation `{Funext} {σ : Signature}
135+
{A : Carriers σ} {w : SymbolType σ}
81136
: ∀ (f g : Operation A w),
82-
(∀ a : FamilyProd A (dom_symboltype w), ap_operation f a = ap_operation g a)
137+
(∀ a : FamilyProd A (dom_symboltype w),
138+
ap_operation f a = ap_operation g a)
83139
-> f = g
84140
:= match w with
85-
| [:s:] => λ f g h, h tt
141+
| [:s:] => λ (f g : A s) p, p tt
86142
| s ::: w' =>
87-
λ f g h, path_forall f g
88-
(λ x, path_forall_ap_operation (f x) (g x) (λ a, h (x,a)))
143+
λ (f g : A s → Operation A w') p,
144+
path_forall f g
145+
(λ x, path_forall_ap_operation (f x) (g x) (λ a, p (x,a)))
89146
end.
90147

148+
(** An [Algebra σ] for a signature [σ] consists of a family [carriers :
149+
Carriers σ] indexed by the sorts [s : Sort σ], and for each symbol
150+
[u : Symbol σ], an operation of type [Operation carriers (σ u)],
151+
where [σ u : SymbolType σ] is the symbol type of [u]. For each
152+
sort [s : Sort σ], [carriers s] is required to be a set. *)
153+
91154
Record Algebra {σ : Signature} : Type := BuildAlgebra
92155
{ carriers : Carriers σ
93156
; operations : ∀ (u : Symbol σ), Operation carriers (σ u)
@@ -97,6 +160,8 @@ Arguments Algebra : clear implicits.
97160

98161
Arguments BuildAlgebra {σ} carriers operations {hset_carriers_algebra}.
99162

163+
(** We have a convenient implicit coercion from an algebra to the
164+
family of carriers. *)
100165
Global Coercion carriers : Algebra >-> Funclass.
101166

102167
Global Existing Instance hset_carriers_algebra.
@@ -119,9 +184,13 @@ Ltac change_issig_algebra A :=
119184
change (operations A) with (issig_algebra A).2.1 in *;
120185
change (carriers A) with (issig_algebra A).1 in *.
121186

187+
(** To find a path between two algebras [A B : Algebra σ] it suffices
188+
to find a path between the carrier families and the operations. *)
189+
122190
Lemma path_algebra `{Funext} {σ} (A B : Algebra σ)
123191
: (∃ (p : carriers A = carriers B),
124-
transport (λ X, ∀ u, Operation X (σ u)) p (operations A) = operations B)
192+
transport (λ X, ∀ u, Operation X (σ u)) p (operations A)
193+
= operations B)
125194
→ A = B.
126195
Proof.
127196
intros [p q].

‎interfaces/ua_congruence.v‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
Require Import
2-
Coq.Unicode.Utf8
32
HoTT.Basics.Equivalences
43
HoTT.HProp
54
HoTT.Types.Universe
@@ -48,12 +47,14 @@ Section congruence.
4847
for all the algebra operations [f]. *)
4948

5049
Record Congruence : Type := BuildCongruence
51-
{ relation_congruence : ∀ (s : Sort σ), relation (A s)
50+
{ relation_congruence
51+
: ∀ (s : Sort σ), relation (A s)
5252
; is_mere_relation_congruence
53-
: ∀ (s : Sort σ), is_mere_relation (A s) (relation_congruence s)
53+
: ∀ (s : Sort σ), is_mere_relation (A s) (relation_congruence s)
5454
; equivalence_congruence
55-
: ∀ (s : Sort σ), Equivalence (relation_congruence s)
56-
; property_congruence : HasCongruenceProperty A relation_congruence }.
55+
: ∀ (s : Sort σ), Equivalence (relation_congruence s)
56+
; property_congruence
57+
: HasCongruenceProperty A relation_congruence }.
5758

5859
Global Existing Instance is_mere_relation_congruence.
5960

‎theory/ua_first_isomorphism.v‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
Require Import
2-
Coq.Unicode.Utf8
32
HoTT.Types.Forall
43
HoTT.Types.Sigma
54
HoTT.Types.Universe

‎theory/ua_homomorphism.v‎

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,14 @@
11
Require Import
2-
Coq.Unicode.Utf8
3-
HoTT.Classes.interfaces.abstract_algebra
4-
HoTTClasses.interfaces.ua_algebra
52
HoTT.Basics.Equivalences
3+
HoTT.Basics.PathGroupoids
64
HoTT.Types.Forall
7-
HoTT.HSet
85
HoTT.Types.Universe
9-
HoTT.Basics.PathGroupoids
10-
HoTT.Tactics
116
HoTT.Types.Record
12-
HoTT.Types.Sigma.
7+
HoTT.Types.Sigma
8+
HoTT.HSet
9+
HoTT.Tactics
10+
HoTT.Classes.interfaces.abstract_algebra
11+
HoTTClasses.interfaces.ua_algebra.
1312

1413
Import algebra_notations ne_list.notations.
1514

‎theory/ua_prod_algebra.v‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
Require Import
2-
Coq.Unicode.Utf8
32
HoTT.Basics.Equivalences
43
HoTT.Types.Forall
54
HoTT.Types.Sigma

‎theory/ua_quotient_algebra.v‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
Require Import
2-
Coq.Unicode.Utf8
32
HoTT.Basics.Equivalences
43
HoTT.Types.Arrow
54
HoTT.Types.Forall

‎theory/ua_second_isomorphism.v‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
Require Import
2-
Coq.Unicode.Utf8
32
HoTT.Types.Sigma
43
HoTT.Types.Universe
54
HoTT.HIT.quotient

‎theory/ua_subalgebra.v‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
Require Import
2-
Coq.Unicode.Utf8
32
HoTT.Basics.Equivalences
43
HoTT.Types.Sigma
54
HoTT.Types.Record

‎theory/ua_third_isomorphism.v‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
Require Import
2-
Coq.Unicode.Utf8
32
HoTT.Types.Universe
43
HoTT.HIT.quotient
54
HoTT.Classes.interfaces.abstract_algebra

0 commit comments

Comments
 (0)