Re: [isabelle] ML style "functors" for Isabelle theories?

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
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: (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

Kind Regards,
Mikhail Chekhov

Attachment: MCATS.png
Description: PNG image

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.