Locus 1.2.0

A new release of Locus has been pushed to github. This version is the most different from any of its predecessors.

• Everything is a set again: the new concrete categories support in this system makes everything as much as possible into structured sets. This allows us to reason about more functions using topos theory and the fundamental topos $Sets^{\to}$.
  • $Sets^{\to}$ itself is a concrete category. Functions $f: A \to B$ have elements which are either input elements of $A$ or output elements of $B$ which can be represented as ordered pairs $(0,a)$ and $(1,b)$ to distinguish rather or not an element is in the input set or the output set. A morphism of functions in $Sets^{\to}$ is then a function on these input and output elements.
  • $Quiv$ is a concrete category whose elements are objects and morphisms. In particular, as categories are enriched quivers, they are again structured sets whose elements are objects and morphisms. Functors are functions of categorical elements.
  • Let $F$ be an arbitrary copresheaf in $Sets^P$. Then its elements are simply section elements $(o,x)$ with $o \in Ob(P)$ and $x \in F(o)$. It follows that structured presheaves are simply structured sets of sections. Section elements are now supported by special classes.
• The new concrete category framework also supports the theory of structure presheaves. Any functor to a concrete category has an udnerlying copresheaf. So it follows for example that a quiver valued functor $F: C \to Quiv$ has an underlying presheaf defined by the mechanism that turns $Quiv$ into a concrete category.
• By the same token we have mechanisms for converting $Rel$ and the category of partial functions into concrete categories, so that functors $f : C \to Rel$ are represented as structure presheaves.
• In order to better support the topos theoretic foundations, our emphasis on $Sets^{\to}$ and set valued functors, the fundamental parts of the system related to $Sets^{\to}$ and the foundational logic of functions are moved into the base folder instead of the elementary folder.
• A whole new and fundamental mechanism for displaying copresheaves is now supported in this version of Locus. It focuses on copresheaves over partial orders, and it displays them in Graphviz like a clustered Hasse diagram. Corresponding to this, a wide variety of new types of copresheaves over partial orders is supported in this version. New mechanisms for handling functional dependencies are provided, and a new class for handling copresheaves over preorders is defined.
• New mechanisms are provided to make morphisms of dependency functors back into dependency functors, and morphisms of copresheaves back into copresheaves. With these new mechanisms we can get a handle on the sufficiency of presheaf topos theory.
• Subobject classifiers are finally provided for all the different topoi in the system, including subobject classifiers of chains which generalize subobject classifiers of functions.
• We have new support for two quivers: which are simply ordered pairs of quivers sharing a common set of edges and objects. In other words, they are quivers which have 2-morphisms between morphisms without any conditions that the morphisms they are between need to be parallel.
• By the same token, we provide a 2-globular set class that provides us with quivers with 2-morphisms that are only between parallel pairs of morphisms. These 2-globular sets can then be used to provide a model of 2-categories.
• We now have support for n-globular sets, n quivers, etc. These are the first in the series of presheaf topos theoretic structures for higher categories. Globular and simplicial sets can be used as models of higher categories, thereby giving them a basis in presheaves.
• The readme was drastically changed and whole sections were removed, dealing with topos theoretic knowledge representation as I have rethought the entire issue. Instead, I leave a new section on geometric philosophy. In this section, I describe how computer science is like geometry and topos theory is the key to understanding computation. I leave the details of that open to further examination, rather then going in to too many specifics as the theory is constantly changing.