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

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

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

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

Author: tslil-topos

packages/catlog/src/dbl/modal/model.rs

@@ -74,7 +74,7 @@ impl MorListData {
 
 /// A model of a modal double theory.
 #[derive(Clone)]
-pub struct ModalDblModel<Kind> {
+pub struct ModalDblModel<Kind: DblTheoryKind> {
     theory: Rc<ModalDblTheory<Kind>>,
     ob_generators: HashFinSet<QualifiedName>,
     mor_generators: ComputadTop<ModalOb, QualifiedName>,
@@ -104,7 +104,7 @@ impl<Kind: DblTheoryKind> ModalDblModel<Kind> {
 
 #[derive(RefCast)]
 #[repr(transparent)]
-struct ModalDblModelObs<Kind>(ModalDblModel<Kind>);
+struct ModalDblModelObs<Kind: DblTheoryKind>(ModalDblModel<Kind>);
 
 impl<Kind: DblTheoryKind> Set for ModalDblModelObs<Kind> {
     type Elem = ModalOb;

packages/catlog/src/dbl/modal/theory.rs

@@ -29,7 +29,7 @@ use indexmap::IndexMap;
 use ref_cast::RefCast;
 
 use crate::dbl::computad::{AVDCComputad, AVDCComputadTop};
-use crate::dbl::theory::{DblTheoryKind, InvalidDblTheory};
+use crate::dbl::theory::{DblTheoryKind, InvalidDblTheory, NonUnital};
 use crate::dbl::{DblTree, InvalidVDblGraph, VDCWithComposites, VDblCategory, VDblGraph};
 use crate::one::computad::{Computad, ComputadTop};
 use crate::validate::{self, Validate};
@@ -258,21 +258,22 @@ pub type ModalMorOp = DblTree<ModalObOp, ModalMorType, ModalNode>;
 /// A modal double theory.
 #[derive(Debug, Derivative)]
 #[derivative(Default(new = "true"))]
-pub struct ModalDblTheory<Kind> {
+pub struct ModalDblTheory<Kind: DblTheoryKind> {
     _kind: PhantomData<Kind>,
     ob_generators: HashFinSet<QualifiedName>,
     arr_generators: ComputadTop<ModalObType, QualifiedName>,
     pro_generators: ComputadTop<ModalObType, QualifiedName>,
     cell_generators: AVDCComputadTop<ModalObType, ModalObOp, ModalMorType, QualifiedName>,
     arr_equations: Vec<PathEq<ModalObType, ModeApp<ModalOp>>>,
     pro_composites: IndexMap<(ModalType, ModalType), ModalMorType>,
+    _unitful_types: Kind::TypesWithUnits<ModalObType>,
     // TODO: Cell equations
 }
 
 /// Set of object types in a modal double theory.
 #[derive(RefCast)]
 #[repr(transparent)]
-pub(super) struct ModalObTypes<Kind>(ModalDblTheory<Kind>);
+pub(super) struct ModalObTypes<Kind: DblTheoryKind>(ModalDblTheory<Kind>);
 
 impl<Kind: DblTheoryKind> Set for ModalObTypes<Kind> {
     type Elem = ModalObType;
@@ -285,7 +286,7 @@ impl<Kind: DblTheoryKind> Set for ModalObTypes<Kind> {
 /// Graph of object types and *basic* morphism types in a modal double theory.
 #[derive(RefCast)]
 #[repr(transparent)]
-struct ModalProedgeGraph<Kind>(ModalDblTheory<Kind>);
+struct ModalProedgeGraph<Kind: DblTheoryKind>(ModalDblTheory<Kind>);
 
 impl<Kind: DblTheoryKind> Graph for ModalProedgeGraph<Kind> {
     type V = ModalObType;
@@ -308,7 +309,7 @@ impl<Kind: DblTheoryKind> Graph for ModalProedgeGraph<Kind> {
 /// Graph of object/morphism types in a modal double theory.
 #[derive(RefCast)]
 #[repr(transparent)]
-pub(super) struct ModalMorTypeGraph<Kind>(ModalDblTheory<Kind>);
+pub(super) struct ModalMorTypeGraph<Kind: DblTheoryKind>(ModalDblTheory<Kind>);
 
 impl<Kind: DblTheoryKind> Graph for ModalMorTypeGraph<Kind> {
     type V = ModalObType;
@@ -337,7 +338,7 @@ impl<Kind: DblTheoryKind> ReflexiveGraph for ModalMorTypeGraph<Kind> {
 /// Graph of object types and *basic* object operations in a modal theory.
 #[derive(RefCast)]
 #[repr(transparent)]
-struct ModalEdgeGraph<Kind>(ModalDblTheory<Kind>);
+struct ModalEdgeGraph<Kind: DblTheoryKind>(ModalDblTheory<Kind>);
 
 impl<Kind: DblTheoryKind> Graph for ModalEdgeGraph<Kind> {
     type V = ModalObType;
@@ -371,7 +372,7 @@ impl<Kind: DblTheoryKind> Graph for ModalEdgeGraph<Kind> {
 /// Category of object types/operations in a modal double theory.
 #[derive(RefCast)]
 #[repr(transparent)]
-pub(super) struct ModalOneTheory<Kind>(ModalDblTheory<Kind>);
+pub(super) struct ModalOneTheory<Kind: DblTheoryKind>(ModalDblTheory<Kind>);
 
 impl<Kind: DblTheoryKind> Category for ModalOneTheory<Kind> {
     type Ob = ModalObType;
@@ -397,7 +398,7 @@ impl<Kind: DblTheoryKind> Category for ModalOneTheory<Kind> {
 /// Virtual double graph of *basic* cells in a modal double theory.
 #[derive(RefCast)]
 #[repr(transparent)]
-struct ModalVDblGraph<Kind>(ModalDblTheory<Kind>);
+struct ModalVDblGraph<Kind: DblTheoryKind>(ModalDblTheory<Kind>);
 
 type ModalVDblComputad<'a, Kind> = AVDCComputad<
     'a,
@@ -626,7 +627,13 @@ impl<Kind: DblTheoryKind> VDCWithComposites for ModalDblTheory<Kind> {
 
     fn composite(&self, path: Path<Self::Ob, Self::Pro>) -> Option<Self::Pro> {
         match path {
-            Path::Id(x) => Some(ShortPath::Zero(x)),
+            Path::Id(x) => {
+                if Kind::has_unit(&self._unitful_types, &x) {
+                    Some(ShortPath::Zero(x))
+                } else {
+                    None
+                }
+            }
             Path::Seq(ms) => {
                 if ms.len() == 1 {
                     Some(ms.head)
@@ -758,3 +765,13 @@ impl<Kind: DblTheoryKind> ModalDblTheory<Kind> {
         self.pro_composites.insert((fst, snd), composite);
     }
 }
+
+impl ModalDblTheory<NonUnital> {
+    /// Adds a unit proarrow for an object type in a non-unital theory.
+    ///
+    /// In a non-unital theory, object types do not automatically have unit
+    /// proarrows (hom types). This method explicitly grants one.
+    pub fn add_unit(&mut self, ob_type: ModalObType) {
+        self._unitful_types.insert(ob_type);
+    }
+}

packages/catlog/src/dbl/theory.rs

@@ -67,7 +67,8 @@
 //! - [Patterson, 2024](crate::refs::DblProducts),
 //!   Section 10: Finite-product double theories
 
-use std::fmt;
+use std::collections::HashSet;
+use std::hash::Hash;
 
 use nonempty::NonEmpty;
 
@@ -98,18 +99,31 @@ mod private {
 /// This trait is [sealed] and cannot be implemented outside this crate.
 ///
 /// [sealed]: https://rust-lang.github.io/api-guidelines/future-proofing.html#sealed-traits-protect-against-downstream-implementations-c-sealed
-pub trait DblTheoryKind: fmt::Debug + private::Sealed {
+pub trait DblTheoryKind: private::Sealed {
     /// Wraps a type to reflect whether values are guaranteed to exist.
     ///
     /// For [`Unital`], this is the identity (`T`).
     /// For [`NonUnital`], this is `Option<T>`.
     type Wrap<T>;
 
+    /// State tracking which object types have unit proarrows.
+    ///
+    /// For [`Unital`], this is `()` (all object types have units).
+    /// For [`NonUnital`], this is `HashSet<X>` (only explicitly
+    /// registered object types have units).
+    type TypesWithUnits<X>: Default;
+
     /// Converts from an `Option` into a wrapped value.
     ///
     /// For [`Unital`], this unwraps with the given message.
     /// For [`NonUnital`], this is the identity.
     fn from_option<T>(opt: Option<T>, msg: &str) -> Self::Wrap<T>;
+
+    /// Does the given object type have a unit proarrow?
+    ///
+    /// For [`Unital`], this always returns `true`.
+    /// For [`NonUnital`], this checks the provided set of unitful types.
+    fn has_unit<Ob: Eq + Hash>(unitful_types: &Self::TypesWithUnits<Ob>, ob: &Ob) -> bool;
 }
 
 /// Unital double theories guarantee that every object type has a hom type.
@@ -121,10 +135,15 @@ pub struct Unital;
 
 impl DblTheoryKind for Unital {
     type Wrap<T> = T;
+    type TypesWithUnits<X> = ();
 
     fn from_option<T>(opt: Option<T>, msg: &str) -> T {
         opt.expect(msg)
     }
+
+    fn has_unit<Ob: Eq + Hash>(_unitful_types: &(), _ob: &Ob) -> bool {
+        true
+    }
 }
 
 /// Set-theoretic double theories make no guarantee that hom types exist.
@@ -136,10 +155,15 @@ pub struct NonUnital;
 
 impl DblTheoryKind for NonUnital {
     type Wrap<T> = Option<T>;
+    type TypesWithUnits<X> = HashSet<X>;
 
     fn from_option<T>(opt: Option<T>, _msg: &str) -> Option<T> {
         opt
     }
+
+    fn has_unit<Ob: Eq + Hash>(unitful_types: &HashSet<Ob>, ob: &Ob) -> bool {
+        unitful_types.contains(ob)
+    }
 }
 
 /// A double theory.

packages/notebook-types/bindings/user_state.ts

@@ -0,0 +1,6 @@
+// This file was generated by [ts-rs](https://github.com/Aleph-Alpha/ts-rs). Do not edit this file manually.
+
+/**
+ * The type/kind of a document, without any associated content.
+ */
+export type DocumentType = "model" | "diagram" | "analysis";