Pseudo-morphisms in essentially algebraic theories

Question

Categories with terminal objects can be written as an essentially algebraic theory or a generalized algebraic theory: There is one sort $M$ with unary operations $\DeclareMathOperator\dom{dom}\dom$, $\DeclareMathOperator\cod{cod}\cod$ and $!$, a binary operation $\circ$ and a nullary operation $1$. There is an automatically derived notion of homomorphisms between these algebras, which when worked out produces functors strictly preserving the terminal object. However, we know that the most natural notion to investigate is functors $F$ such that $F(1) \dashrightarrow 1$ is an isomorphism.

Is there a way to systematically derive a notion of "weak" homomorphisms of EAT/GAT algebras, such that when applied to categories or even bicategories, produces the "correct" notion of functors? I would imagine it to be easier using generalized algebraic theories, since objects now appear in the sorts. Is there anything in the literature discussing this?

Answer 1

This is one of the main themes of Arkor–Bourke–Ko's paper Enhanced 2-categorical structures, two-dimensional limit sketches and the symmetry of internalisation. In particular, in §5, the authors introduce the notion of enhanced limit 2-sketch, which is a two-dimensional generalisation of the notion of limit sketch (a concept equally expressive to that of an essentially algebraic theory), together with their models and weak morphisms.

For instance, there is an enhanced limit 2-sketch for pseudocategories (Example 5.13 ibid.), whose models in the 2-category of categories are pseudo double categories, and whose pseudo/lax/colax morphisms are precisely the usual notion of pseudo/lax/colax functors of pseudo double categories.