带额外结构与同态的集合定义：结构约束及同态定义问询

假设的结构定义 #

首先给出如下定义：

Structure : (M : Type l -> Type l) -> Type (lsuc l)
Structure M = Σ (Type l) (λ A -> M A)

目标：定义同态类型 #

我们希望定义如下类型：

homomorphism :
  {M : Type l -> Type l} -> (sA sB : Structure M)
  (f : sA.fst -> sB.fst) -> Type l

使得homomorphism (A , MA) (B , MB) f表示函数f是从A到B的、保留由M指定的额外结构的映射（目前尚未形式化“额外结构”与“保留”的概念）。

示例 #

当M A = A -> A -> A时，Structure M对应所有Magma（原群）的类型，此时homomorphism (A , _*A_) (B , _*B_) f就表示f是从A到B的Magma同态。

现有定义的局限与问题提出 #

维基百科的同态定义仅在M A由A上的函数构成时才做了形式化，这一限制过于严格。但如果不对Structure M施加约束，就无法实现我们想要的通用同态定义，因此提出以下两个问题：

1. 可以对Structure M施加哪些合适且合理的约束？（“合理”指排除投机取巧方案，例如直接要求存在以Structure M为对象的范畴并手动指定态射类型）
2. homomorphism的具体定义应当是什么样的？

补充说明：假设univalence公理成立，Id (Structure M) (A , MA) (B , MB)已经接近需求，因为可以从中提取出双射的同态函数。

内容的提问来源于stack exchange，提问作者HPSmash77