I'm in the process of designing a better "logic framework" for BananaCats. Why do I seem limited to Type Theory (which is extremely "low level" for lack of better description). I don't care about most of the stuff talked about in the various books on type theory. All I care about is Category Theory (mostly) and various proofs in those books. What are the drawbacks to just implementing a C++ class called "Category", "Object", "Arrow", "Functor", and so on… Essentially implement everything needed to do every proof in a given textbook?
As you can tell I'm not a fan of taking the bare bones basics and creating another Coq. It seems like we've done all we can do there. If I need natural numbers, say I'll just implement an "Integer" class, for example. If I want to prove Yoneda, I'd need composition, taking elements, natural maps, etc., each concept hard-coded as much as is reasonable.
Below is a 90% visual proof of (one part of) Yoneda's Lemma, that is in a "final stage" of the proof. For example, a reader of the proof might have to go through several diagram changes in a slide show before arriving at this point.
There is a note in the picture, which demonstrates a text accompaniment to the drawing, but as you might have guessed, if I can somehow encode this visually using CD's, I will.
One feature that needs to be hard-coded is if the user takes an element of a set, and there are set-like map arrows (arrows that maybe are subclasses of C++ class type SetMap, or "is a set map" is one of their properties, or however it should be implemented); then, the result of mapping that element to elements in the codomain sets (which might be several in a diagram), is auto-populated, with the correct LaTeX markup in labels which straddle the respective codomain nodes. That was an example of what I mean.
I hope I'm clear enough on this. So, without re-inventing the wheel, how should one proceed, if they definitely want to avoid such low-levelness as described in the various type theories?
Best Answer
There is no higher level view other than perhaps the Type Theory - Category Theory correspondence mentioned in the comments.
As a solution to this problem, I recommend learning the Coq proof assistant langauge called Gallina. With knowledge of it comes knowledge of type theory itself.
I remcommend Coq over Isabelle for a programmer, as naturally later you may wish to extend Coq using the OCaml API or modifying Coq's open source code itself. Isabelle doesn't seem to be as modifiable.