Commit 2025-08-06 01:34 59fa465e

feat: define morphism type StarMonoidHom (#27763) This defines star-preserving monoid homomorphisms between star monoids. The primary motivation for these morphisms is to provide a target type for morphisms which induce a corresponding morphism between the unitary groups in a star monoid. Without this type, there is no concrete type for unitary.map and we end up resorting to morphisms classes instead, which is suboptimal. See Zulip for the problem which motivated the creation of this type.