src/Algebras_ch4.v

   1 (******************************************************************************)
   2 (* Chapter 4: Algebras                                                        *)
   3 (*                                                                            *)
   4 (*   This formalizes for arbitrary algebras what Awodey does for groups in    *)
   5 (*   chapter 4                                                                *)
   6 (******************************************************************************)
   7
   8 Generalizable All Variables.
   9 Require Import Preamble.
  10
  11 (* very handy *)
  12 (*
  13 Fixpoint listOfTypesToType (args:list Type)(ret:Type) : Type :=
  14   match args with
  15   | nil  => ret
  16   | a::b => a -> listOfTypesToType b ret
  17   end.
  18 *)
  19 (*
  20 Section Algebras.
  21
  22 Local Notation "a :: b" := (vec_cons a b).
  23 Local Notation "[]"     := (vec_nil).
  24 Local Notation "[ a ]"  := (a::[]).
  25
  26 Structure Signature : Type :=
  27 { sig_sort       : Type
  28 ; sig_op         : 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)
  32 }.
  33
  34 Section DerivedOperations.
  35
  36   Context (sig:Signature).
  37
  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))*)
  41   (*FIXME*)
  42   }.
  43
  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.
  48     Defined.
  49   Definition length : Arity -> nat.
  50     intro a; destruct a; auto.
  51     Defined.
  52
  53   Definition arity_get (n:nat)(a:Arity)(pf:lt n (length a)) : sig_sort sig.
  54     destruct a.
  55     refine (@vec_get (sig_sort sig) _ v n pf).
  56     Defined.
  57
  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).
  66
  67   (* an identity is a pair of derived operations, WLOG having the same arity *)
  68   Record Identity :=
  69   { id_arity  : Arity
  70   ; id_result : sig_sort sig
  71   ; id_op1    : DerivedOperation id_arity id_result
  72   ; id_op2    : DerivedOperation id_arity id_result
  73   }.
  74
  75   Definition Relations := list Identity.
  76
  77   Inductive Satisfies : Algebra -> Relations -> Prop :=.
  78
  79 End DerivedOperations.
  80
  81 (* TO DO: an algebra of signature [s] in monoidal category [c] *)
  82 (* FIXME: generators-and-relations *)
  83 (* see also example 9.36 *)
  84
  85 (*
  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.
  89 *)
  90 (*
  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
  93 }.
  94
  95 Structure AlgebraSortedAlgebra {sig}{rel}(algss:@AlgebraSortedSignature sig rel) : Type :=
  96 {
  97 }.
  98 Definition AlgebraSortedSignature_is_Signature : forall sig rel, AlgebraSortedSignature sig rel -> Signature sig rel.
  99   Defined.
 100   Coercion AlgebraSortedSignature_is_Signature : AlgebraSortedSignature >-> Signature.
 101 *)
 102
 103 (* algebraically axiomatized monoidal categories *)
 104 Record AMCat :=
 105 { amcat_ob                   : Type
 106 ; amcat_I                    : amcat_ob
 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)
 109
 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)
 112
 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)
 118
 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)
 123
 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)
 126
 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
 143 }.
 144
 145 (* To Do: AMCat is an algebraically-sorted signature *)
 146
 147 (* any given level of the Coq universe hierarchy satisfies the algebraic laws for a monoidal category *)
 148 Definition Coq_AMCat : AMCat.
 149  refine
 150  {| amcat_ob        := Type
 151   ; amcat_I         := unit
 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.
 170   Defined.
 171   Coercion amcat_ob : AMCat >-> Sortclass.
 172
 173 (* To do: arbitrary algebras internal to an MCat *)
 174
 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 *)
 178
 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.
 189
 190 (* what we call a category is actually an AMCat-enriched-Cat *)
 191 (*
 192 Record Cat (V:AMCat) :=
 193 { cat_ob             :   Type
 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 _ _ _
 202 }.
 203
 204 Close Scope amcat_scope.
 205
 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.
 211
 212
 213
 214
 215
 216 (* a monoidal category enriched in an AMCat *)
 217 Record MCat (V:AMCat) :=
 218 { mcat_cat : Cat V
 219 (* plus monoidal structure *)
 220 }.
 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.*)
 226
 227
 228 (*
 229  * Given an MCat we can derive an AMCat, which can then in turn have
 230  * internal stuff –- this is essentially the first externalization
 231  * functor (I₀).
 232  *)
 233 (*
 234 Definition AMCat_from_MCat `(C:MCat V) : AMCat.
 235   Defined.
 236 *)
 237
 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! *)
 241
 242 *)
 243 End Algebras.
 244 *)
 245