I also got some progress on figuring out what the categorical semantics of my little system is. It's looking like I don't need to add too much extra junk to the existing local cartesian closed structure that needs to be there already for dependent types. I mainly need a monoid object M × M → M ← 1 with a suitable action, and maybe a couple other isomorphisms that have to hold. The action follows noticing that Hom(Γ, M), the hom-set of generalized elements of M, inherits a monoid structure for every particular Γ, and the condition is then that this monoid acts *Γ on the objects of the slice category C/Γ. I have a feeling there is a snappy category-theory way of saying this without explicitly naming the Γs, but damned if I know what it is. The snappiest I can get is saying that it's a functor Hom(Γ, M) → End(C/Γ). The only other condition I feel pretty confident about goes like this: since we live in an LCCC, there is for every Γ a right adjoint ∀ to the pullback functor along the projection Γ × M → Γ. Now ∀ takes types over Γ × M to types over Γ. This type constructor (which is what you'd use to interpret world quantification) definitely ought to be compatible with the monoid action: I think what I need to require is some canonical isomorphism (∀ f) *Γ p ≅ ∀ (f *Γ×M (p ∘ π1)) for any world p : Γ → M and type f : X → Γ × M.
Played some music in Morewood later, saw a lot of people walking back and forth with boxes. I wonder if they're students moving in for the summer, or hired. student-age staff installing the microfridges for the freshmen or something. I did see a lot of microfridges.