Previously in Agda we had constructed equalizers in Lambek${\begin{array}{}\end{array}}^{𝙳}$ using sigma types. Further, equalizers form subobjects, which may be comprehended as maps from a type into a subobject classifier.

I believe in our formalization we want to generalize this idea to a broader class of subobjects, maybe even all of them. That is, we could define a subobject classifying grammar $\mathrm{\Omega }$. Then we can internally define any predicate on a grammar $𝑔$ via a term $𝑝:𝑔⊢\mathrm{\Omega }$.

That is, forall $𝑤:\text{String}$ we have $⟦\mathrm{\Omega }⟧(𝑤)≔\text{𝗁𝖯𝗋𝗈𝗉}$, and

The code for this is nearly identical to the definition of equalizers as sigma types, and I have even built a translation of the equalizers code that is defined with this as its foundation. I have not yet tested if either implementation is preferable.

It isn’t yet clear how to best expose this sort of construct syntactically. I suppose you could assume some subobject classifying grammar, but then I don’t know if you can then reap the benefits of the propositions internally. That is, how do you reflect the proposition that two terms are equal in the internal language of propositions rather than the external one?

If nothing else, this code gives me a reusable interface to axiomatize smaller, sandboxed ways in which I’d like to internalize certain types of propositions (such as “two terms are equal” or “does not begin with the character $𝑐$”).

The hope for this code is that it lets me inductively prove the follow last soundness of Kleene star.