1 (******************************************************************************)
2 (* Chapter 4: Algebras *)
4 (* This formalizes for arbitrary algebras what Awodey does for groups in *)
6 (******************************************************************************)
8 Generalizable All Variables.
9 Require Import Preamble.
10 Require Import General.
14 Fixpoint listOfTypesToType (args:list Type)(ret:Type) : Type :=
17 | a::b => a -> listOfTypesToType b ret
23 Local Notation "a :: b" := (vec_cons a b).
24 Local Notation "[]" := (vec_nil).
25 Local Notation "[ a ]" := (a::[]).
27 Structure Signature : Type :=
30 ; sig_arity_len : sig_op -> nat
31 ; sig_result : sig_op -> sig_sort
32 ; sig_arity : forall op:sig_op, vec sig_sort (sig_arity_len op)
35 Section DerivedOperations.
37 Context (sig:Signature).
39 Structure Algebra : Type :=
40 { alg_carrier : sig_sort sig -> Type
41 (*; alg_op : forall op:sig_op sig, listOfTypesToType (map alg_carrier (sig_arity sig op)) (alg_carrier (sig_result sig op))*)
45 (* the "arity" of an operation in a multi-sorted signature is a finite list of sorts *)
46 Definition Arity := { n:nat & vec (sig_sort sig) n }.
47 Definition mkArity {n:nat} : vec (sig_sort sig) n -> Arity.
48 intros v; exists n; auto.
50 Definition length : Arity -> nat.
51 intro a; destruct a; auto.
54 Definition arity_get (n:nat)(a:Arity)(pf:lt n (length a)) : sig_sort sig.
56 refine (@vec_get (sig_sort sig) _ v n pf).
59 (* See Bergman, Invitation to Universal Algebra, Def 8.9.1 *)
60 Inductive DerivedOperation : Arity -> sig_sort sig -> Type :=
61 | do_op : forall op:sig_op sig, DerivedOperation (mkArity (sig_arity sig op)) (sig_result sig op)
62 | do_projection : forall (a:Arity)(n:nat)(pf:lt n (length a)), DerivedOperation a (arity_get n a pf)
63 | do_compose : forall n a b c, VecOfDerivedOperations n a b -> DerivedOperation (mkArity b) c -> DerivedOperation a c
64 with VecOfDerivedOperations : forall n:nat, Arity -> vec (sig_sort sig) n -> Type :=
65 | vodo_nil : forall a, VecOfDerivedOperations 0 a []
66 | vodo_cons : forall a b n v, DerivedOperation a b -> VecOfDerivedOperations n a v -> VecOfDerivedOperations (S n) a (b::v).
68 (* an identity is a pair of derived operations, WLOG having the same arity *)
71 ; id_result : sig_sort sig
72 ; id_op1 : DerivedOperation id_arity id_result
73 ; id_op2 : DerivedOperation id_arity id_result
76 Definition Relations := list Identity.
78 Inductive Satisfies : Algebra -> Relations -> Prop :=.
80 End DerivedOperations.
82 (* TO DO: an algebra of signature [s] in monoidal category [c] *)
83 (* FIXME: generators-and-relations *)
84 (* see also example 9.36 *)
87 An Algebra-Sorted-Signature consists of an algebra of sorts and a
88 collection of operations such that each operations's arity is a list
89 of elements of the sort algebra.
92 Structure AlgebraSortedSignature `(relations_on_sort_algebra : Relations signature_of_sort_algebra) : Type :=
93 { algss_sort_algebra : Algebra signature_of_sort_algebra relations_on_sort_algebra
96 Structure AlgebraSortedAlgebra {sig}{rel}(algss:@AlgebraSortedSignature sig rel) : Type :=
99 Definition AlgebraSortedSignature_is_Signature : forall sig rel, AlgebraSortedSignature sig rel -> Signature sig rel.
101 Coercion AlgebraSortedSignature_is_Signature : AlgebraSortedSignature >-> Signature.
104 (* algebraically axiomatized monoidal categories *)
108 ; amcat_hom : amcat_ob -> amcat_ob -> Type where "a ~> b" := (amcat_hom a b)
109 ; amcat_oprod : amcat_ob -> amcat_ob -> amcat_ob where "a ⊗ b" := (amcat_oprod a b)
111 ; amcat_eqv : ∀ a b, a~>b -> a~>b -> Prop where "f ~~ g" := (amcat_eqv _ _ f g)
112 ; amcat_eqv_eqv : ∀ a b, Equivalence (amcat_eqv a b)
114 ; amcat_id : ∀ a, a~>a
115 ; amcat_comp : ∀ a b c, a~>b -> b~>c -> a~>c where "f >>> g" := (amcat_comp _ _ _ f g)
116 ; amcat_mprod : ∀ a b c d, a~>b -> c~>d -> (a⊗c)~>(b⊗d) where "a × b" := (amcat_mprod _ _ _ _ a b)
117 and "f ⋉ A" := (f × (amcat_id A))
118 and "A ⋊ f" := ((amcat_id A) × f)
120 ; amcat_comp_respects : ∀ a b c, Proper (amcat_eqv a b ==> amcat_eqv b c ==> amcat_eqv a c) (amcat_comp _ _ _)
121 ; amcat_left_identity : forall `(f:a~>b), (amcat_id a >>> f) ~~ f
122 ; amcat_right_identity : forall `(f:a~>b), f >>> amcat_id b ~~ f
123 ; amcat_associativity : forall `(f:a~>b)`(g:b~>c)`(h:c~>d), (f >>> g) >>> h ~~ f >>> (g >>> h)
125 ; amcat_mprod_preserves_id : forall a b, (amcat_id a) × (amcat_id b) ~~ (amcat_id (a⊗b))
126 ; amcat_mprod_preserves_comp : forall `(f1:a1~>b1)`(g1:b1~>c1)`(f2:a2~>b2)`(g2:b2~>c2), (f1>>>g1)×(f2>>>g2) ~~ (f1×f2)>>>(g1×g2)
128 ; amcat_cancell : ∀ a, amcat_I⊗a ~> a
129 ; amcat_cancelr : ∀ a, a⊗amcat_I ~> a
130 ; amcat_assoc : ∀ a b c, (a⊗b)⊗c ~> a⊗(b⊗c)
131 ; amcat_uncancell : ∀ a, a ~> amcat_I⊗a
132 ; amcat_uncancelr : ∀ a, a ~> a⊗amcat_I
133 ; amcat_unassoc : ∀ a b c, a⊗(b⊗c) ~> (a⊗b)⊗c
134 ; amcat_cancell_uncancell : ∀ a, amcat_uncancell a >>> amcat_cancell a ~~ amcat_id a
135 ; amcat_cancell_uncancelr : ∀ a, amcat_uncancelr a >>> amcat_cancelr a ~~ amcat_id a
136 ; amcat_assoc_unassoc : ∀ a b c, amcat_unassoc a b c >>> amcat_assoc _ _ _ ~~ amcat_id _
137 ; amcat_cancell_natural : forall `(f:a~>b), amcat_uncancell _ >>> (amcat_id _ × f) ~~ f >>> amcat_uncancell _
138 ; amcat_cancelr_natural : forall `(f:a~>b), amcat_uncancelr _ >>> (f × amcat_id _) ~~ f >>> amcat_uncancelr _
139 ; amcat_assoc_natural : forall `(f:a1~>b1)`(g:a2~>b2)`(h:a3~>b3),
140 amcat_assoc _ _ _ >>> (f × (g × h)) ~~ ((f × g) × h) >>> amcat_assoc _ _ _
141 ; amcat_pentagon : forall a b c d, amcat_assoc a b c ⋉ d >>> amcat_assoc a _ d >>> a ⋊ amcat_assoc b c d
142 ~~ amcat_assoc _ c d >>> amcat_assoc a b _
143 ; amcat_triangle : forall a b, amcat_cancelr a ⋉ _ ~~ amcat_assoc _ _ _ >>> _ ⋊ amcat_cancell b
146 (* To Do: AMCat is an algebraically-sorted signature *)
148 (* any given level of the Coq universe hierarchy satisfies the algebraic laws for a monoidal category *)
149 Definition Coq_AMCat : AMCat.
153 ; amcat_hom := fun a b => a->b
154 ; amcat_oprod := fun a b => prod a b
155 ; amcat_eqv := fun a b f g => forall q, (f q)=(g q)
156 ; amcat_id := fun a x => x
157 ; amcat_comp := fun a b c f g => g ○ f
158 ; amcat_mprod := fun a b c d f g => fun x => let (x1,x2) := x in ((f x1),(g x2))
159 ; amcat_cancell := fun a => fun x => let (x1,x2) := x in x2
160 ; amcat_cancelr := fun a => fun x => let (x1,x2) := x in x1
161 ; amcat_assoc := fun a b c => fun x => let (x12,x3) := x in let (x1,x2) := x12 in (x1,(x2,x3))
162 ; amcat_uncancell := fun a => fun x => (tt,x)
163 ; amcat_uncancelr := fun a => fun x => (x,tt)
164 ; amcat_unassoc := fun a b c => fun x => let (x1,x23) := x in let (x2,x3) := x23 in ((x1,x2),x3)
165 |}; intros; simpl; auto; try destruct q; auto; try destruct p; auto; try destruct p; auto.
166 apply Build_Equivalence; simpl;
167 [ unfold Reflexive; intros; auto
168 | unfold Symmetric; intros; symmetry; auto
169 | unfold Transitive; intros; rewrite H; auto ].
170 unfold Proper; unfold respectful; intros; rewrite H; rewrite H0; reflexivity.
172 Coercion amcat_ob : AMCat >-> Sortclass.
174 (* To do: arbitrary algebras internal to an MCat *)
176 (* hrm, internalization is sort of a (primitive-recursive) operation
177 on signatures –- you take a signature for X and produce the signature
178 of MCats with an internal X *)
180 Delimit Scope amcat_scope with amcat.
181 Open Scope amcat_scope.
182 Notation "a ~> b" := (amcat_hom _ a b) : amcat_scope.
183 Notation "a ⊗ b" := (amcat_oprod _ a b) : amcat_scope.
184 Notation "f ~~ g" := (amcat_eqv _ _ _ f g) : amcat_scope.
185 Notation "f >>> g" := (amcat_comp _ _ _ _ f g) : amcat_scope.
186 Notation "a × b" := (@amcat_mprod _ _ _ _ _ a b) : amcat_scope.
187 Notation "f ⋉ A" := (f × (amcat_id _ A)) : amcat_scope.
188 Notation "A ⋊ f" := ((amcat_id _ A) × f) : amcat_scope.
189 Notation "'I'" := (amcat_I _) : amcat_scope.
191 (* what we call a category is actually an AMCat-enriched-Cat *)
193 Record Cat (V:AMCat) :=
195 ; cat_hom : cat_ob -> cat_ob -> V where "a ⇒ b" := (cat_hom a b)
196 ; cat_id : ∀ a , I ~> a ⇒ a
197 ; cat_ecomp : ∀ a b c , (a ⇒ b)⊗(b ⇒ c) ~> (a ⇒ c)
198 ; cat_left_identity : ∀ a b , cat_id a ⋉ (a ⇒ b) >>> cat_ecomp _ _ _ ~~ amcat_cancell _ _
199 ; cat_right_identity : ∀ a b , (a ⇒ b) ⋊ cat_id b >>> cat_ecomp _ _ _ ~~ amcat_cancelr _ _
200 ; cat_associativity : ∀ a b c d, amcat_unassoc _ _ _ (_ ⇒ _) >>> cat_ecomp _ _ _ ⋉ (c ⇒ d) >>> cat_ecomp _ _ _ ~~
201 (a ⇒ b) ⋊ cat_ecomp _ _ _ >>> cat_ecomp _ _ _
202 ; cat_comp := fun a b c f g => amcat_uncancell V _ >>> (amcat_mprod V I (a⇒ b) I (b⇒ c) f g) >>> cat_ecomp _ _ _
205 Close Scope amcat_scope.
207 Delimit Scope cat_scope with cat.
208 Notation "a ~> b" := (cat_hom _ a b) : cat_scope.
209 Notation "f ~~ g" := (@amcat_eqv _ _ _ f g) : cat_scope.
210 Notation "f >>> g" := (@cat_comp _ _ _ _ _ f g) : cat_scope.
211 Close Scope cat_scope.
217 (* a monoidal category enriched in an AMCat *)
218 Record MCat (V:AMCat) :=
220 (* plus monoidal structure *)
222 (*Notation "a ⊗ b" := (amcat_oprod _ a b) : cat_scope.
223 Notation "a × b" := (amcat_mprod _ _ _ _ _ a b) : cat_scope.
224 Notation "f ⋉ A" := (f × (amcat_id _ A)) : cat_scope.
225 Notation "A ⋊ f" := ((amcat_id A) × f) : cat_scope.
226 Notation "'I'" := (amcat_I _) : cat_scope.*)
230 * Given an MCat we can derive an AMCat, which can then in turn have
231 * internal stuff –- this is essentially the first externalization
235 Definition AMCat_from_MCat `(C:MCat V) : AMCat.
239 (* need CategoryWithProducts, then use a category enriched in a category with products to get products of categories *)
240 (* it's really only functors we need to change: get rid of the general notion, and allow only EFunctors *)
241 (* then we can more easily do functor-categories! *)