feature: allow non-unital theories to be meaningfully non-unital

[tslil-topos]

Before this change the blanket impl impl<Kind: DblTheoryKind> VDCWithComposites for ModalDblTheory<Kind> would always give a unit pro-arrow to every object, which is semantically too powerful.

In order to allow particular modal double theories to specify which objects ("types") are unital ("categorical" in their semantics) we need to track some state on the struct.

The approach taken in this change is to extend the API of DblTheoryKind minimally with type TypesWithUnits<X>: Default; and

    fn has_unit<Ob: Eq + Hash>(
        unitful_types: &Self::TypesWithUnits<Ob>,
        ob: &Ob,
    ) -> bool;

In the case of Unital theories TypesWithUnits<X> is (), but for NonUnital it's HashSet. In the latter case ModalDblTheory grows pub fn add_unit(&mut self, ob_type: ModalObType).

This change is needed to do #1167 and #1162 correctly

[epatters]

Thanks for giving this a go!

I confess that when writing the RFC I didn't think through how units should be handled in the non-unital case since in all of our currently envisaged examples, none of the objects will have units. And in light of my comment below, there is some subtlety in handling the situation where some-but-not-all objects are specified to have units.

Unless you strongly feel otherwise, since we don't yet have any motivating examples, I'd recommend that we not yet go down this path, and for now make the simplifying assumption that non-unital theories have no chosen units.

[epatters]

While this probably isn't legibly documented anywhere (sorry, we've got some mathematical debt to clear here), the modalities (double monads or comonads) on the theory are assumed to be strict, i.e., to preserve loose composites and units. In that case, this check isn't sufficient since if $x$ has a unit $\mathrm{id}_x$, then so does $Tx$, namely \id_{Tx} = T \id_x (GitHub math is laughably broken).

[epatters]

It feels strange to me bake this assumption about how units would be checked into NonUnital, independent of the model implementation itself.

[tslil-topos]

Thanks for the review @epatters !

sorry, i'm not sure i understand what you mean here. At the risk of saying something you well understand for the exercise of my trying to reason through your intentions: what's really going on in this change is that the VDCWithComposites implementation would always formally supply units for objects, regardless of the theory type.

The code currently has ModalDblTheory -> VDCWithComposites -> DblTheory (there's also a not-relevant-for-this-story ModalDblTheory -> VDblCategory). Unfortunately that intermediate step currently always adds units (formally)

I'm not sure what the intention of the code was, or what we want the final form to be, but looking around it's currently sufficient (and i thought mathematically correct) to make that "always formally add units" step conditional on something and that something (i thought) could only be the subset of objects for which we want units---is there some more general condition that you had in mind? I'm not sure i see how this interferes with modalities, even if they are strict. There are no lawfulness checks that i can see --- the code constructs ShortPath::map to be correct---, and in any event those checks would be "if this object has a unit then that unit is preserved by the endofunctor", right?

Maybe the best approach here is to rethink this path from ModalDblTheory to DblTheory in the non-unital case in specific, and avoid piling on more and more concessions for this approach. I leave it to you to decide how, if at all, you want a change like this to be shaped (maybe we change non-unital to mean "no units ever at" at the type level (eg enum Bottom {} instead of the current Option)). Once we've thought through how we want to proceed, we can address things like #1185.

For now, as much as it is theoretically incorrect, i think i can continue on #1167 for example without having this change in there and just pretend that the units are never added.