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.
13 Fixpoint listOfTypesToType (args:list Type)(ret:Type) : Type :=
16 | a::b => a -> listOfTypesToType b ret
22 Local Notation "a :: b" := (vec_cons a b).
23 Local Notation "[]" := (vec_nil).
24 Local Notation "[ a ]" := (a::[]).
26 Structure Signature : Type :=
29 ; sig_arity_len : sig_op -> nat
30 ; sig_result : sig_op -> sig_sort
31 ; sig_arity : forall op:sig_op, vec sig_sort (sig_arity_len op)
34 Section DerivedOperations.
36 Context (sig:Signature).
38 Structure Algebra : Type :=
39 { alg_carrier : sig_sort sig -> Type
40 (*; alg_op : forall op:sig_op sig, listOfTypesToType (map alg_carrier (sig_arity sig op)) (alg_carrier (sig_result sig op))*)
44 (* the "arity" of an operation in a multi-sorted signature is a finite list of sorts *)
45 Definition Arity := { n:nat & vec (sig_sort sig) n }.
46 Definition mkArity {n:nat} : vec (sig_sort sig) n -> Arity.
47 intros v; exists n; auto.
49 Definition length : Arity -> nat.
50 intro a; destruct a; auto.
53 Definition arity_get (n:nat)(a:Arity)(pf:lt n (length a)) : sig_sort sig.
55 refine (@vec_get (sig_sort sig) _ v n pf).
58 (* See Bergman, Invitation to Universal Algebra, Def 8.9.1 *)
59 Inductive DerivedOperation : Arity -> sig_sort sig -> Type :=
60 | do_op : forall op:sig_op sig, DerivedOperation (mkArity (sig_arity sig op)) (sig_result sig op)
61 | do_projection : forall (a:Arity)(n:nat)(pf:lt n (length a)), DerivedOperation a (arity_get n a pf)
62 | do_compose : forall n a b c, VecOfDerivedOperations n a b -> DerivedOperation (mkArity b) c -> DerivedOperation a c
63 with VecOfDerivedOperations : forall n:nat, Arity -> vec (sig_sort sig) n -> Type :=
64 | vodo_nil : forall a, VecOfDerivedOperations 0 a []
65 | vodo_cons : forall a b n v, DerivedOperation a b -> VecOfDerivedOperations n a v -> VecOfDerivedOperations (S n) a (b::v).
67 (* an identity is a pair of derived operations, WLOG having the same arity *)
70 ; id_result : sig_sort sig
71 ; id_op1 : DerivedOperation id_arity id_result
72 ; id_op2 : DerivedOperation id_arity id_result
75 Definition Relations := list Identity.
77 Inductive Satisfies : Algebra -> Relations -> Prop :=.
79 End DerivedOperations.
81 (* TO DO: an algebra of signature [s] in monoidal category [c] *)
82 (* FIXME: generators-and-relations *)
83 (* see also example 9.36 *)
86 An Algebra-Sorted-Signature consists of an algebra of sorts and a
87 collection of operations such that each operations's arity is a list
88 of elements of the sort algebra.
91 Structure AlgebraSortedSignature `(relations_on_sort_algebra : Relations signature_of_sort_algebra) : Type :=
92 { algss_sort_algebra : Algebra signature_of_sort_algebra relations_on_sort_algebra
95 Structure AlgebraSortedAlgebra {sig}{rel}(algss:@AlgebraSortedSignature sig rel) : Type :=
98 Definition AlgebraSortedSignature_is_Signature : forall sig rel, AlgebraSortedSignature sig rel -> Signature sig rel.
100 Coercion AlgebraSortedSignature_is_Signature : AlgebraSortedSignature >-> Signature.
103 (* algebraically axiomatized monoidal categories *)
107 ; amcat_hom : amcat_ob -> amcat_ob -> Type where "a ~> b" := (amcat_hom a b)
108 ; amcat_oprod : amcat_ob -> amcat_ob -> amcat_ob where "a ⊗ b" := (amcat_oprod a b)
110 ; amcat_eqv : ∀ a b, a~>b -> a~>b -> Prop where "f ~~ g" := (amcat_eqv _ _ f g)
111 ; amcat_eqv_eqv : ∀ a b, Equivalence (amcat_eqv a b)
113 ; amcat_id : ∀ a, a~>a
114 ; amcat_comp : ∀ a b c, a~>b -> b~>c -> a~>c where "f >>> g" := (amcat_comp _ _ _ f g)
115 ; amcat_mprod : ∀ a b c d, a~>b -> c~>d -> (a⊗c)~>(b⊗d) where "a × b" := (amcat_mprod _ _ _ _ a b)
116 and "f ⋉ A" := (f × (amcat_id A))
117 and "A ⋊ f" := ((amcat_id A) × f)
119 ; amcat_comp_respects : ∀ a b c, Proper (amcat_eqv a b ==> amcat_eqv b c ==> amcat_eqv a c) (amcat_comp _ _ _)
120 ; amcat_left_identity : forall `(f:a~>b), (amcat_id a >>> f) ~~ f
121 ; amcat_right_identity : forall `(f:a~>b), f >>> amcat_id b ~~ f
122 ; amcat_associativity : forall `(f:a~>b)`(g:b~>c)`(h:c~>d), (f >>> g) >>> h ~~ f >>> (g >>> h)
124 ; amcat_mprod_preserves_id : forall a b, (amcat_id a) × (amcat_id b) ~~ (amcat_id (a⊗b))
125 ; 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)
127 ; amcat_cancell : ∀ a, amcat_I⊗a ~> a
128 ; amcat_cancelr : ∀ a, a⊗amcat_I ~> a
129 ; amcat_assoc : ∀ a b c, (a⊗b)⊗c ~> a⊗(b⊗c)
130 ; amcat_uncancell : ∀ a, a ~> amcat_I⊗a
131 ; amcat_uncancelr : ∀ a, a ~> a⊗amcat_I
132 ; amcat_unassoc : ∀ a b c, a⊗(b⊗c) ~> (a⊗b)⊗c
133 ; amcat_cancell_uncancell : ∀ a, amcat_uncancell a >>> amcat_cancell a ~~ amcat_id a
134 ; amcat_cancell_uncancelr : ∀ a, amcat_uncancelr a >>> amcat_cancelr a ~~ amcat_id a
135 ; amcat_assoc_unassoc : ∀ a b c, amcat_unassoc a b c >>> amcat_assoc _ _ _ ~~ amcat_id _
136 ; amcat_cancell_natural : forall `(f:a~>b), amcat_uncancell _ >>> (amcat_id _ × f) ~~ f >>> amcat_uncancell _
137 ; amcat_cancelr_natural : forall `(f:a~>b), amcat_uncancelr _ >>> (f × amcat_id _) ~~ f >>> amcat_uncancelr _
138 ; amcat_assoc_natural : forall `(f:a1~>b1)`(g:a2~>b2)`(h:a3~>b3),
139 amcat_assoc _ _ _ >>> (f × (g × h)) ~~ ((f × g) × h) >>> amcat_assoc _ _ _
140 ; amcat_pentagon : forall a b c d, amcat_assoc a b c ⋉ d >>> amcat_assoc a _ d >>> a ⋊ amcat_assoc b c d
141 ~~ amcat_assoc _ c d >>> amcat_assoc a b _
142 ; amcat_triangle : forall a b, amcat_cancelr a ⋉ _ ~~ amcat_assoc _ _ _ >>> _ ⋊ amcat_cancell b
145 (* To Do: AMCat is an algebraically-sorted signature *)
147 (* any given level of the Coq universe hierarchy satisfies the algebraic laws for a monoidal category *)
148 Definition Coq_AMCat : AMCat.
152 ; amcat_hom := fun a b => a->b
153 ; amcat_oprod := fun a b => prod a b
154 ; amcat_eqv := fun a b f g => forall q, (f q)=(g q)
155 ; amcat_id := fun a x => x
156 ; amcat_comp := fun a b c f g => g ○ f
157 ; amcat_mprod := fun a b c d f g => fun x => let (x1,x2) := x in ((f x1),(g x2))
158 ; amcat_cancell := fun a => fun x => let (x1,x2) := x in x2
159 ; amcat_cancelr := fun a => fun x => let (x1,x2) := x in x1
160 ; amcat_assoc := fun a b c => fun x => let (x12,x3) := x in let (x1,x2) := x12 in (x1,(x2,x3))
161 ; amcat_uncancell := fun a => fun x => (tt,x)
162 ; amcat_uncancelr := fun a => fun x => (x,tt)
163 ; amcat_unassoc := fun a b c => fun x => let (x1,x23) := x in let (x2,x3) := x23 in ((x1,x2),x3)
164 |}; intros; simpl; auto; try destruct q; auto; try destruct p; auto; try destruct p; auto.
165 apply Build_Equivalence; simpl;
166 [ unfold Reflexive; intros; auto
167 | unfold Symmetric; intros; symmetry; auto
168 | unfold Transitive; intros; rewrite H; auto ].
169 unfold Proper; unfold respectful; intros; rewrite H; rewrite H0; reflexivity.
171 Coercion amcat_ob : AMCat >-> Sortclass.
173 (* To do: arbitrary algebras internal to an MCat *)
175 (* hrm, internalization is sort of a (primitive-recursive) operation
176 on signatures –- you take a signature for X and produce the signature
177 of MCats with an internal X *)
179 Delimit Scope amcat_scope with amcat.
180 Open Scope amcat_scope.
181 Notation "a ~> b" := (amcat_hom _ a b) : amcat_scope.
182 Notation "a ⊗ b" := (amcat_oprod _ a b) : amcat_scope.
183 Notation "f ~~ g" := (amcat_eqv _ _ _ f g) : amcat_scope.
184 Notation "f >>> g" := (amcat_comp _ _ _ _ f g) : amcat_scope.
185 Notation "a × b" := (@amcat_mprod _ _ _ _ _ a b) : amcat_scope.
186 Notation "f ⋉ A" := (f × (amcat_id _ A)) : amcat_scope.
187 Notation "A ⋊ f" := ((amcat_id _ A) × f) : amcat_scope.
188 Notation "'I'" := (amcat_I _) : amcat_scope.
190 (* what we call a category is actually an AMCat-enriched-Cat *)
192 Record Cat (V:AMCat) :=
194 ; cat_hom : cat_ob -> cat_ob -> V where "a ⇒ b" := (cat_hom a b)
195 ; cat_id : ∀ a , I ~> a ⇒ a
196 ; cat_ecomp : ∀ a b c , (a ⇒ b)⊗(b ⇒ c) ~> (a ⇒ c)
197 ; cat_left_identity : ∀ a b , cat_id a ⋉ (a ⇒ b) >>> cat_ecomp _ _ _ ~~ amcat_cancell _ _
198 ; cat_right_identity : ∀ a b , (a ⇒ b) ⋊ cat_id b >>> cat_ecomp _ _ _ ~~ amcat_cancelr _ _
199 ; cat_associativity : ∀ a b c d, amcat_unassoc _ _ _ (_ ⇒ _) >>> cat_ecomp _ _ _ ⋉ (c ⇒ d) >>> cat_ecomp _ _ _ ~~
200 (a ⇒ b) ⋊ cat_ecomp _ _ _ >>> cat_ecomp _ _ _
201 ; cat_comp := fun a b c f g => amcat_uncancell V _ >>> (amcat_mprod V I (a⇒ b) I (b⇒ c) f g) >>> cat_ecomp _ _ _
204 Close Scope amcat_scope.
206 Delimit Scope cat_scope with cat.
207 Notation "a ~> b" := (cat_hom _ a b) : cat_scope.
208 Notation "f ~~ g" := (@amcat_eqv _ _ _ f g) : cat_scope.
209 Notation "f >>> g" := (@cat_comp _ _ _ _ _ f g) : cat_scope.
210 Close Scope cat_scope.
216 (* a monoidal category enriched in an AMCat *)
217 Record MCat (V:AMCat) :=
219 (* plus monoidal structure *)
221 (*Notation "a ⊗ b" := (amcat_oprod _ a b) : cat_scope.
222 Notation "a × b" := (amcat_mprod _ _ _ _ _ a b) : cat_scope.
223 Notation "f ⋉ A" := (f × (amcat_id _ A)) : cat_scope.
224 Notation "A ⋊ f" := ((amcat_id A) × f) : cat_scope.
225 Notation "'I'" := (amcat_I _) : cat_scope.*)
229 * Given an MCat we can derive an AMCat, which can then in turn have
230 * internal stuff –- this is essentially the first externalization
234 Definition AMCat_from_MCat `(C:MCat V) : AMCat.
238 (* need CategoryWithProducts, then use a category enriched in a category with products to get products of categories *)
239 (* it's really only functors we need to change: get rid of the general notion, and allow only EFunctors *)
240 (* then we can more easily do functor-categories! *)