(* categories, fully axiomatised *) axiom = Gen + HOL_Gen + datatype ('obj, 'arr) cat = Cat ('obj set) "['obj, 'obj] => 'arr set" "'arr => 'obj" "'arr => 'obj" "'obj => 'arr" "['arr, 'arr] => 'arr" consts c_objs :: "('obj, 'arr) cat => ('obj set)" c_arrf :: "('obj, 'arr) cat => (['obj, 'obj] => 'arr set)" c_arrs :: "('obj, 'arr) cat => ('arr set)" c_srcf :: "('obj, 'arr) cat => ('arr => 'obj)" c_tgtf :: "('obj, 'arr) cat => ('arr => 'obj)" c_ida :: "('obj, 'arr) cat => ('obj => 'arr)" c_cmp :: "('obj, 'arr) cat => (['arr, 'arr] => 'arr)" primrec "c_srcf (Cat ob a s t i c) = s" primrec "c_tgtf (Cat ob a s t i c) = t" primrec "c_ida (Cat ob a s t i c) = i" primrec "c_cmp (Cat ob a s t i c) = c" primrec "c_objs (Cat ob a s t i c) = ob" primrec "c_arrf (Cat ob a s t i c) = a" primrec c_arrs "c_arrs (Cat ob a s t i c) = (UN o1 : ob. UN o2 : ob. a o1 o2)" (* conditions for category *) consts cat_ok, cat_st, cat_idst, cat_cmp, cat_idcmp, cat_assoc :: "('obj, 'arr) cat => bool" primrec cat_st "cat_st (Cat ob af s t i c) = (ALL o1 : ob. ALL o2 : ob. ALL a : af o1 o2. s a = o1 & t a = o2)" primrec cat_idst "cat_idst (Cat ob a s t i c) = (ALL o1 : ob. s (i o1) = o1 & t (i o1) = o1 & i o1 : a o1 o1)" primrec cat_cmp "cat_cmp (Cat ob a s t i c) = (ALL o1 : ob. ALL o2 : ob. ALL o3 : ob. ALL a12 : a o1 o2. ALL a23 : a o2 o3. c a23 a12 : a o1 o3)" primrec cat_idcmp "cat_idcmp (Cat ob af s t i c) = (ALL o1 : ob. ALL o2 : ob. ALL a : af o1 o2. c (i o2) a = a & c a (i o1) = a)" primrec cat_assoc "cat_assoc (Cat ob a s t i c) = (ALL o1 : ob. ALL o2 : ob. ALL o3 : ob. ALL o4 : ob. ALL a12 : a o1 o2. ALL a23 : a o2 o3. ALL a34 : a o3 o4. c a34 (c a23 a12) = c (c a34 a23) a12)" defs cat_ok_def "cat_ok c == cat_st c & cat_idst c & cat_cmp c & cat_idcmp c & cat_assoc c" (* functors and natural transformations *) datatype ('obj1, 'arr1, 'obj2, 'arr2) funct = Fun (('obj1, 'arr1) cat) (('obj2, 'arr2) cat) "'obj1 => 'obj2" "'arr1 => 'arr2" datatype ('obj1, 'arr1, 'obj2, 'arr2) nat_trf = NT (('obj1, 'arr1, 'obj2, 'arr2) funct) (('obj1, 'arr1, 'obj2, 'arr2) funct) "'obj1 => 'arr2" consts (* source and target categories of a functor, or of a nat trf *) f_src :: "('obj1, 'arr1, 'obj2, 'arr2) funct => ('obj1, 'arr1) cat" n_srcc :: "('obj1, 'arr1, 'obj2, 'arr2) nat_trf => ('obj1, 'arr1) cat" f_tgt :: "('obj1, 'arr1, 'obj2, 'arr2) funct => ('obj2, 'arr2) cat" n_tgtc :: "('obj1, 'arr1, 'obj2, 'arr2) nat_trf => ('obj2, 'arr2) cat" (* source and target functors of a nat trf *) n_srcf, n_tgtf :: "('obj1, 'arr1, 'obj2, 'arr2) nat_trf => ('obj1, 'arr1, 'obj2, 'arr2) funct" (* functor's arrow and object functions *) f_af :: "('obj1, 'arr1, 'obj2, 'arr2) funct => ('arr1 => 'arr2)" f_obf :: "('obj1, 'arr1, 'obj2, 'arr2) funct => ('obj1 => 'obj2)" n_h :: "('obj1, 'arr1, 'obj2, 'arr2) nat_trf => 'obj1 => 'arr2" (* conditions on functor, nat trf *) fun_o, fun_a, fun_st, fun_id, fun_cmp, fun_cat_ok, fun_ok :: "('obj1, 'arr1, 'obj2, 'arr2) funct => bool" nt_o, nt_same, nt_comm, nt_fun_ok, nt_ok :: "('obj1, 'arr1, 'obj2, 'arr2) nat_trf => bool" primrec "f_src (Fun cat1 cat2 objf arrf) = cat1" primrec "f_tgt (Fun cat1 cat2 objf arrf) = cat2" primrec "f_af (Fun cat1 cat2 objf arrf) = arrf" primrec "f_obf (Fun cat1 cat2 objf arrf) = objf" primrec fun_o "fun_o (Fun cat1 cat2 objf arrf) = (ALL o1 : c_objs cat1. objf o1 : c_objs cat2)" primrec fun_a "fun_a (Fun cat1 cat2 objf arrf) = (ALL o1 : c_objs cat1. ALL o2 : c_objs cat1. ALL a : c_arrf cat1 o1 o2. arrf a : c_arrf cat2 (objf o1) (objf o2))" primrec fun_st "fun_st (Fun cat1 cat2 objf arrf) = (ALL a : c_arrs cat1. c_srcf cat2 (arrf a) = objf (c_srcf cat1 a) & c_tgtf cat2 (arrf a) = objf (c_tgtf cat1 a))" primrec fun_id "fun_id (Fun cat1 cat2 objf arrf) = (ALL o1 : c_objs cat1. arrf (c_ida cat1 o1) = c_ida cat2 (objf o1))" primrec fun_cmp "fun_cmp (Fun cat1 cat2 objf arrf) = (ALL a1 : c_arrs cat1. ALL a2 : c_arrs cat1. c_srcf cat1 a2 = c_tgtf cat1 a1 --> c_cmp cat2 (arrf a2) (arrf a1) = arrf (c_cmp cat1 a2 a1))" primrec fun_cat_ok "fun_cat_ok (Fun cat1 cat2 objf arrf) = (cat_ok cat1 & cat_ok cat2)" defs fun_ok_def "fun_ok c == fun_o c & fun_a c & fun_id c & fun_cmp c & fun_cat_ok c" primrec "n_srcf (NT fun1 fun2 h) = fun1" primrec "n_tgtf (NT fun1 fun2 h) = fun2" primrec n_srcc "n_srcc (NT fun1 fun2 h) = f_src fun1" primrec n_tgtc "n_tgtc (NT fun1 fun2 h) = f_tgt fun1" primrec "n_h (NT fun1 fun2 h) = h" (* same source and target categories *) primrec nt_same "nt_same (NT fun1 fun2 h) = (f_src fun1 = f_src fun2 & f_tgt fun1 = f_tgt fun2)" primrec nt_o "nt_o (NT fun1 fun2 h) = (ALL o1 : c_objs (f_src fun1). h o1 : c_arrf (f_tgt fun1) (f_obf fun1 o1) (f_obf fun2 o1))" primrec nt_comm "nt_comm (NT fun1 fun2 h) = (let sc = f_src fun1 ; tc = f_tgt fun1 in ALL o1 : c_objs sc. ALL o2 : c_objs sc. ALL a : c_arrf sc o1 o2. c_cmp tc (h o2) (f_af fun1 a) = c_cmp tc (f_af fun2 a) (h o1))" primrec nt_fun_ok "nt_fun_ok (NT fun1 fun2 h) = (fun_ok fun1 & fun_ok fun2)" defs nt_ok_def "nt_ok c == nt_o c & nt_same c & nt_comm c & nt_fun_ok c" (* identity, composition of functors and natural transformations *) consts func_id :: "('obj, 'arr) cat => ('obj, 'arr, 'obj, 'arr) funct" func_cmp :: "[('obj2, 'arr2, 'obj3, 'arr3) funct, ('obj1, 'arr1, 'obj2, 'arr2) funct] => ('obj1, 'arr1, 'obj3, 'arr3) funct" nat_id :: "('obj1, 'arr1, 'obj2, 'arr2) funct => ('obj1, 'arr1, 'obj2, 'arr2) nat_trf" nat_cmp :: "[('obj1, 'arr1, 'obj2, 'arr2) nat_trf, ('obj1, 'arr1, 'obj2, 'arr2) nat_trf] => ('obj1, 'arr1, 'obj2, 'arr2) nat_trf" defs func_id "func_id cat == Fun cat cat id id" func_cmp "func_cmp fun2 fun1 == Fun (f_src fun1) (f_tgt fun2) (f_obf fun2 o f_obf fun1) (f_af fun2 o f_af fun1)" nat_id "nat_id fun == NT fun fun (c_ida (f_tgt fun) o f_obf fun)" nat_cmp "nat_cmp nt2 nt1 == NT (n_srcf nt1) (n_tgtf nt2) (%a. c_cmp (n_tgtc nt1) (n_h nt2 a) (n_h nt1 a))" end