*To*: cl-isabelle-users at lists.cam.ac.uk, mahonybp at tpg.com.au*Subject*: Re: [isabelle] ML style "functors" for Isabelle theories?*From*: Mikhail Chekhov <mikhail.chekhov.w at gmail.com>*Date*: Tue, 21 Jul 2020 23:26:35 +0300

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

**Attachment:
MCATS.png**

**Follow-Ups**:**Re: [isabelle] ML style "functors" for Isabelle theories?***From:*Mikhail Chekhov

- Previous by Date: Re: [isabelle] get set of (proper) divisors for a specific number?
- Next by Date: [isabelle] Isabelle standard mathematics library, HOL-Analysis and HOL-Algebra: articles/references?
- Previous by Thread: [isabelle] ML style "functors" for Isabelle theories?
- Next by Thread: Re: [isabelle] ML style "functors" for Isabelle theories?
- Cl-isabelle-users July 2020 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list