From: "Dr. Brendan Patrick Mahony" <mahonybp@tpg.com.au>

Isabelle’s mathematical structuring facilities, classes and locales, have well known scopes that preclude some otherwise attractive modelling approaches.

For example, the AFP has three approaches to category theory that model a category’s carrier classes of objects and arrows as types.

https://www.isa-afp.org/browser_info/current/AFP/Category/document.pdf <https://www.isa-afp.org/browser_info/current/AFP/Category/document.pdf>

https://www.isa-afp.org/entries/Category2.html <https://www.isa-afp.org/entries/Category2.html>

https://www.isa-afp.org/entries/Category3.html

Besides the pure mathematical constraints this places of the classes of category instances (much of which is I guess inherent to the use of HOL), this also brings a degree of applied mathematical pain in that it would frequently be convenient in a practical reasoning sense to model objects and arrows as classes of types, so as to make use of a type overloaded arrow composition operator and enjoy all the reasoning safety benefits of HOL strong typing.

This can of course be done for any desired category, some examples

Set:

class cat_obj = small

typedef

('a, 'b) cat_arrow = "{ f :: ('a::cat_obj) ⇒ ('b::cat_obj). True}"

by (auto)

definition

cat_compose :: "('a::cat_obj, 'b::cat_obj) cat_arrow ⇒ ('b, 'c::cat_obj) cat_arrow ⇒ ('a, 'c) cat_arrow"

where

"cat_compose f g = Abs_cat_arrow ((Rep_cat_arrow g) ∘ (Rep_cat_arrow f))"

definition

cat_id :: "('a::cat_obj, 'a) cat_arrow"

where

"cat_id = Abs_cat_arrow id"

lemma cat_left_id:

"cat_compose cat_id a = a"

by (auto simp add: cat_compose_def cat_id_def Abs_cat_arrow_inverse Rep_cat_arrow_inverse)

lemma cat_right_id:

"cat_compose a cat_id = a"

by (auto simp add: cat_compose_def cat_id_def Abs_cat_arrow_inverse Rep_cat_arrow_inverse)

lemma cat_comp_assoc:

"cat_compose (cat_compose a b) c = cat_compose a (cat_compose b c)"

by (auto simp add: cat_compose_def cat_id_def Abs_cat_arrow_inverse Rep_cat_arrow_inverse comp_assoc)

Grp:

class cat_obj = group_add

typedef (overloaded)

('a, 'b) cat_arrow = "{ f :: ('a::cat_obj) ⇒ ('b::cat_obj). (∀ a b. f (a + b) = f a + f b) }"

apply (rule_tac x = "(λ a. 0)" in exI)

apply (auto)

done

definition

cat_compose :: "('a::cat_obj, 'b::cat_obj) cat_arrow ⇒ ('b, 'c::cat_obj) cat_arrow ⇒ ('a, 'c) cat_arrow"

where

"cat_compose f g = Abs_cat_arrow ((Rep_cat_arrow g) ∘ (Rep_cat_arrow f))"

lemma cat_compose_wf:

assumes

a1: "f ∈ { f :: ('b::cat_obj) ⇒ ('c::cat_obj). (∀ a b. f (a + b) = f a + f b) }" and

a2: "g ∈ { f :: ('a::cat_obj) ⇒ ('b::cat_obj). (∀ a b. f (a + b) = f a + f b) }"

shows

"f ∘ g ∈ { f :: ('a::cat_obj) ⇒ ('c::cat_obj). (∀ a b. f (a + b) = f a + f b) }"

using assms

by (auto)

definition

cat_id :: "('a::cat_obj, 'a) cat_arrow"

where

"cat_id = Abs_cat_arrow id"

lemma cat_left_id:

"cat_compose cat_id a = a"

by (auto simp add: cat_compose_def cat_id_def Abs_cat_arrow_inverse Rep_cat_arrow_inverse)

lemma cat_right_id:

"cat_compose a cat_id = a"

by (auto simp add: cat_compose_def cat_id_def Abs_cat_arrow_inverse Rep_cat_arrow_inverse)

lemma cat_comp_assoc:

"cat_compose (cat_compose a b) c = cat_compose a (cat_compose b c)"

by (auto simp add: cat_compose_def cat_id_def Rep_cat_arrow_inverse comp_assoc

Abs_cat_arrow_inverse [OF cat_compose_wf [OF Rep_cat_arrow Rep_cat_arrow]])

This is nice for “using" these categories in modelling efforts, but not so nice for doing category “theory” and in particular developing a class of category operators and associated properties that are shared by all by all instances. You know, the sort of instancing power offered by classes and locales.

My naive solution is to define an axiomatised “signature” theory for category theory and do all the abstract (repeatable) reasoning there.

theory Category_Sig

imports

Main

begin

class

cat_obj

typedecl

('a, 'b) cat_arrow

consts

cat_compose :: "('a::cat_obj, 'b::cat_obj) cat_arrow ⇒ ('b, 'c::cat_obj) cat_arrow ⇒ ('a, 'c) cat_arrow"

consts

cat_id :: "('a::cat_obj, 'a) cat_arrow"

axiomatization where

cat_left_id: "cat_compose cat_id a = a" and

cat_right_id: "cat_compose a cat_id = a" and

cat_comp_assoc: "cat_compose (cat_compose a b) c = cat_compose a (cat_compose b c)"

context

begin

notation

cat_compose (infixr "∘⇩♭" 55)

notation

cat_id ("ι⇩♭")

qualified lemma inv_uniq:

assumes

a1: "f ∘⇩♭ g = cat_id" and

a2: "h ∘⇩♭ f = cat_id"

shows

"g = h"

proof -

have

"g = ι⇩♭ ∘⇩♭ g"

by (rule cat_left_id [symmetric])

also have "…

= (h ∘⇩♭ f) ∘⇩♭ g"

by (simp add: a2)

also have "…

= h ∘⇩♭ (f ∘⇩♭ g)"

by (simp add: cat_comp_assoc)

also have "…

= h ∘⇩♭ ι⇩♭"

by (simp add: a1)

also have "…

= h"

by (rule cat_right_id)

finally show

"g = h"

by (this)

qed

end

end

Then I can use textual replacement to make copies of the signature theory and "drop in” the appropriate definitions to replace the axiomatisations, global replace the \<flat> subscript, etc … to get the desired instance theories.

Any pointers to more sophisticated approaches? (Should note that categories are not my actual algebraic target here, just a convenient and easily understood example)

It seems to suggest to me that it would be nice to have a theory “functor” facility analogous to the structure “functor" facility of standard ML.

Does anyone have any pointers to (Isabelle) work in this direction?

I noted with interest an MMT/LF paper in the recent LFMTP workshop that seemed to be suggesting something similar, but I think a bit more general

@inproceedings{Roux:2020a,

Author = {Navid Roux and Florian Rabe},

Booktitle = {Logical Frameworks and Meta Languages: Theory and Practice},

Title = {Diagram Operators in a Logical Framework},

Year = {2020}}

From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>

Dear Brendan Patrick Mahony/All,

I would like to make a side remark for your question.

At one point, I did think about developing an infrastructure for the

definition of generic 'meta-theories' by using implicit quantification over

types modelled via the use of the schematic type variables (see

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-September/msg00095.html

and,

more importantly, the reply). For this to work, one would need to write

Isabelle/ML infrastructure that can generate an 'instance' of (for example)

category theory on demand for a given set of constants like group,

group_hom, etc. This is certainly possible (see the screenshot and please

ignore all aspects not directly related to the software infrastructure that

the screenshot is meant to demonstrate), but, for me, the amount of effort

required seemed to be unsurmountable. The advantage of this approach is

that it does not require any new axioms to be added to Isabelle/HOL.

Since then, I have converged on the idea that it is best to use an

extension of HOL (e.g. ZFC in HOL or HOTG) and allow the 'meta-theory' and

the 'object-theory' to coexist using only the standard techniques. In the

context of such extensions, this means that the 'object-theory' will be

limited to some reasonably small set (e.g. V(ω+ω)). Of course, once such

theory is developed, one might be able to develop an infrastructure for the

translation of concepts across isomorphisms, under the limitation of size

only (I am not certain how easy and well automated this could become). I

have been doing some work in this direction for a certain time. The

foundational part of my development is available here:

https://gitlab.com/user9716869/czh_foundations (more applied concepts are

still in a very transient state and not available publicly). However, most

likely, this work will be superseded by HOTG that is being developed by

Alexander Krauss, Kevin Kappelmann and Joshua Chen (see

https://bitbucket.org/cezaryka/tyset/src).

Kind Regards,

Mikhail Chekhov

MCATS.png

From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>

Dear All,

I forgot to provide references for my previous post in this thread. It was

not my intention to put an emphasis on the references, as they contain

well-known foundational material, but I do feel awkward for omitting them

from my post and feel the need to correct this.

Last updated: Dec 05 2021 at 23:19 UTC