Investigations into the Idris2 proof assistant and some formalizations

Is there a proof assistant which combines the best aspects of Coq/Rocq and Agda? We would like the construction of proof-terms be done in a natural deduction style, close to actual mathematical practice (at least for the proofs of category theory). This is different at once from the top-down method of constructing proofs in Coq/Rocq and from the emacs interface of Agda and its system of refinement, filling holes, etc.

Dependent type theory - extensions of type theories such as used in Ocaml and Haskell - seems to us philosophically, computationally, logically and practically the best foundation for mathematics. The elegant Idris 2 proof assistant - which we could call an idealized version of Agda (but with linear types!) - seems to be most promising. It is simple and versatile and can work with emacs, vim or nano. Could we use it as a basis to develop our natural deduction style interactive theorem proving?

Idris 2 with its REPL in fact feel like a enhanced version of Ocaml or Haskell (upon which it is based) - but it is not so easy to install (we are running it on an Ubuntu virtual machine in whih we need rlwrap to get command history).

We can seemlessly formalize category theory in Idris 2 (it seems this can be done in a simpler and more direct way than in Coq/Rocq) - a fact which is already of logico-philosophical significance.

https://github.com/owl77/Idris2_formalizations/blob/main/ct.idr

In this module we define general categories, opposite categories, the category of "sets", the empty, singleton and canonical category with two elements, product categories terminal objects, functors and natural transformations, point out the necessity of extensionality to define the category of sets and the need to postulate identity conditions for natural transformations. We prove that functors between categories A and B and their natural transformations form a category. As a result we can define the category of presheaves over a given category A and the yoneda embedding. We define ´diagonal functors, cones and limits. And the composition of functors, the identity functors, the category of categories and the "whiskering operations" (Godement product) and use this to define adjunctions in terms of the triangle identities. There are several interesting points regarding the coherence of natural transformation equality relative to functor identity (cf. transport in Hott). We believe that Iris 2 is the best (and most efficient) dependent-type based proof assistant for this task, once one understands how to use rewrite and Refl.

Consider how we prove that any two terminal objects in a category are isomorphic. To do this we show first that given a terminal object T its canonical morphism to itself must be id_T (this is the lemma1 term). This is how in our natural deduction extension of Idris we would construct the lemma1 term in the way a mathematician would prove the result. 

1 c : Cat Hyp
2 a : obj C Hyp 
3 t : terminal c a Hyp
4 t : forall (x: obj c), exists (g : hom c (x,a)), forall (h: hom c (x,a)), h = g Expand 3
5 t a : exists (g : hom c(a,a)), forall (h : hom c(a,a)), h = g Inst 4,2
6 snd (ta) : forall (h : hom c (a,a)), h = fst (ta) Sigma type stuff
7 id c a : hom c (a,a) By def
8 (snd (ta)) (id c a) : id c a = fst (ta) Inst 6,7
9 (c : Cat)(a : obj c)(t : terminal ca), (snd (ta)) (id c a) : (c: Cat) -> (a : obj c) -> (t : terminal c a) -> h = fst (ta) QED

New section in "Hegel and Modern Topology"

The most recent version of "Hegel and Modern Topology" includes a new 4 page section: "Formalization of Hegel's Logic of Concept".

Very short note on formal concepts in science

From whence do we get the impression that some mathematical models are closer to physical and spatio-temporal intuition,  more down to earth and intimately tied to concrete applications, while others hover close to the heights of allegedly less useful  'abstract-nonsense' ? The real numbers and differential equations, these are seen as tied to dynamic-geometric intuition and of vast applicability and interest in engineering and science.  But abstract algebra and category theory appear to have no direct relevance to applicable mathematical models or to their kind of concrete geometric-dynamic intuition. We present here a few short speculations.

Perhaps the abstract models do capture fundamental levels of reality (maybe even more fundamental than the so-called concrete spatio-temporal ones) and what is required is first of all the methodic development of a special kind of intuition or cognition to grasp the planes of reality which they model (maybe something like Goethe's method is called for?). And then further models are required which can effect a mediation or transfer between these two levels, or at least allow a continuity or gradual deformation between concrete spatio-temporal reality and higher levels of reality.

A beautiful illustration of such a meditation and construction is furnished by the double fibration in Penrose's twistor theory which allows a mediation and transfer between physically significant objects on Minkowski space and abstract cohomological objects on the complex algebraic variety $\mathbb{P}^3$.This operation allows solutions to conformally invariant differential equations on spacetime (e.g., Maxwell's equations, Yang-Mills, or linearized gravity) to be identified exactly with Cech or Dolbeault cohomology classes on specific regions of twistor space. This appears to have been Penrose's attempt to give a geometric (topological) interpretation of quantum non-locality. 

Another illustration is the theory of $\mathcal{D}$-modules which presents a mediation between derived categories (and monoidal categories) and concrete models of systems of partial differential equations.

The idea of Kant's schematism of the pure concepts of the understanding can be interpreted as finding the mediation between logic and geometry (including mathematical physics). This is of immense contemporary significance as we find versions of Kantian schematism in topos theory, homotopy type theory and in areas involving monoidal categories in algebra, geometry and physics and in linear logic and computer science. 

There is also apparently a mediation and transition between the theory of bifurcations of smooth vector fields, fundamental  and ubiquitous in concrete applied mathematics,  and monoidal category and operad theory. See also Physics, Topology, Logic and Computation: A Rosetta Stone by John C. Baez and Mike Stay.

An objection can be raised that our concrete allegedly intuitive mathematical models are themselves quite abstract but are only perceived as immediate and intuitive in our present cultural context by a deliberate forgetting of the complexity of their cognitive-historical past and genesis. For instance real numbers are constructed from the rationals by quite abstract, cardinality increasing, procedures involving equivalence classes and identification. And the same goes for the concepts of continuity, differentiability and so forth. Surely the ancient Greeks had other forms of intuitive perception and concreteness in their geometry, physics and engineering. We answer this objection by our arguments that the fundamental dynamic and geometric-topological intuitions of modern science were in fact identical to those of ancient Greece. It is the modern foundations in terms of Dedekind cuts and $\epsilon$s and $\delta$s that can be critiqued from a philosophical and logical point of view and alternative foundations (locales, realizability topoi, synthetic differential geometry, homotopy type theory) can be defended which are also more aligned to the theory of space and change found for instance in Aristotle's Physics.