coq - 如何理解Setoid对类的定义？

Question

我无法理解以下 Coq 类别定义(定义 here )，它涉及 Setoid。而且我不明白为什么 Setoid 是必要的或它在这里的作用。

Class Category O `{!Arrows O} `{∀ x y: O, Equiv (x ⟶ y)}
 `{!CatId O} `{!CatComp O}: Prop :=
  { arrow_equiv :> ∀ x y, Setoid (x ⟶ y)
  ; comp_proper :> ∀ x y z, Proper ((=) ==> (=) ==> (=)) (comp x y z)
  ; comp_assoc :> ArrowsAssociative O
  ; id_l :> ∀ x y, LeftIdentity (comp x y y) cat_id
  ; id_r :> ∀ x y, RightIdentity (comp x x y) cat_id }.
      (* note: no equality on objects. *)

到目前为止我学到的类别的基本概念只需要

1. 对象之间有箭头，
2. 箭头组合(尊重结合性)和
3. 身份箭头存在并表现。

我知道 Setoid 是关于等价类的，但是我看不出 Setoids 是从哪里来的。有人可以帮忙解释一下上面的定义，并解释一下与没有 Setoids 的通常类别定义的区别吗？

Answer 1

让我引用 J. Gross、A. Chlipala、D.I. 的论文中的 setoids 小节(第 2.4 节)。斯皮瓦克 -- Experience Implementing a Performant Category-Theory Library in Coq (2014):

A setoid [5] is a carrier type equipped with an equivalence relation; a map of setoids is a function between the carrier types and a proof that the function respects the equivalence relations of its domain and codomain. Many authors [11, 12, 15, 18] choose to use a setoid of morphisms, which allows for the definition of the category of set(oid)s, as well as the category of (small) categories, without assuming functional extensionality, and allows for the definition of categories where the objects are quotient types.

上面提到的 [12] 来源是 Math-Classes 库。然而，作者随后提出警告:

However, there is significant overhead associated with using setoids everywhere, which can lead to slower compile times. Every type that we talk about needs to come with a relation and a proof that this relation is an equivalence relation. Every function that we use needs to come with a proof that it sends equivalent elements to equivalent elements. Even worse, if we need an equivalence relation on the universe of “types with equivalence relations,” we need to provide a transport function between equivalent types that respects the equivalence relations of those types.