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