Primarily, this a request to check Fitch-style derivations in the file,
This is not trivial. The reflexiveness derivation contains over 300 steps.
It is fine if no one steps up. I ask only because it is often difficult to see one's own errors in such detailed work.
As for "the philosophy" involved, the stackexchange community has little love for my views. For me, at least, this is a simple fact. Others may not recognize my writing style.
I will only retain a membership for a short time.
Nevertheless, the topic is one which has been of interest to category theorists (or, perhaps, to homotopy type theorists more specifically). In 2019 Quanta published the article,
making great claims concerning the nature of mathematics relative to equality statements. The article illustrates the basic idea behind the work using a pretty graphic. The graphic is based upon a straightforward theorem from algebraic topology about the contractibility of sets in real spaces where every two points can be joined by a straight line segment.
By analogy, the "terms" of an equivalence relation correspond to the endpoints of line segments. The line segments essentially encode how the terms of its endpoints are substitutable for one another.
Essentially, this is a "topological gluing." Recognized as such, it becomes ubiquitous across mathematics. Differential manifolds, for example, are often described as "gluing" small patches of real spaces together with coordinate charts.
The technical details of such gluings always involve transitivity in termwise descriptions.
By contrast, my work lies effectively within the symbolic domain. Hence, the Fitch-style derivations.
I am an autodidact without many resources. Verification --- or any constructive suggestions --- would be appreciated.