Locus 1.4

The newest Locus version has been released to github. I have made several changes to make this program better organized.

• I have added special support for dealing with copresheaves over product and coproduct categories. A copresheaf over a product category $F: C \times D \to Sets$ is a simultaneously a bifunctor and a copresheaf. Support for the hom functor $Hom : C^{op} \times C \to Sets$ is provided with this new framework so for example we can deal with the Yoneda embedding. Support for copresheaves over coproducts is provided by index sums.
• Several improvements have been made in the compositional quivers framework introduced and developed in Locus 1.3. As mentioned previously, the presheaf topos theory of categories now has two components: the theory of Yoneda embeddings and the theory of compositional quivers.
• Corresponding to the support for hom bicopresheaves, we also have new classes to deal with the functor of points and its dual, the basis of representable presheaves and copresheaves used in the Yoneda embedding.
• Recall the definition of the arrow category $Arrow(C)$. Then this can be defined as a category whose objects are morphisms of $C$ and whose morphisms are pairs $(f,g)$ of morphisms that form a commuting diagram, but I feel the more categorical approach is to construct this using the functor category $Hom(T_2,C)$ so the arrow categories framework has been rewritten to be this way. In particular, the to-natural-transformation method can be applied to morphisms in arrow categories.
• In the same vein of making things more categorical, I have become a fan of Lawvere metrics. The distances framework is now based upon them, and $\mathbb{R}^{\infty}_+$ enriched categories. Distances should be studied by reference to certain types of enriched categories.
• I have provided support for cones and cocones as special types of natural transformations. This should be make the categorical implementation of limits/colimits easier. Set cones and cocones are also special types of morphisms of presheaves.
• The entire implementation of functors and presheaves in this program had to be changed on a basic level to help support structure presheaves. Functors are based upon the get-object and get-morphism multimethods while presheaves use the get-set and get-function multimethods. Structure presheaves implement both, so they are like functors and presheaves at the same time.
• I actually implemented section preorders using the section-preorder method. This is something I have talked about here but it wasn't converted into code until now. In the future this will be integrated with the category of elements of a presheaf.
• Among the first functors implemented in the structure presheaves framework are partial copresheaves which are functors to the category of sets and partial maps and relational copresheaves which are functors to $Rel$. I've known for a while that I would want to implement functors to $Rel$ but I didn't have a framework that felt quite right until now with the structure presheaves system. With structure presheaves everything feels quite right.
• Functors from monoids to the category of partial sets are now called PSets rather then PartialActionSystems because it always makes sense to abbreviate things you use a lot.
• We now have support for copresheaves of monoids and other structure copresheaves. The copresheaves of monoids will make way for other nice constructions like presheaves of abelian groups and presheaves of modules.

There is more to be done, but the one thing that remains clear is our strong committment to presheaf topos theory. Presheaves are the means by which we model computation.