哪些公理可以安全地添加到辅酶Q中？

问：

这个问题是要求提供参考或解释。 主要思想是：如果我从Coq的标准库中添加每个公理会怎样？ 这会引起矛盾，还是它们相互适应得很好？ 除了标准的Coq库之外，还有哪些关于Coq的其他可靠信息来源？（我看到了一堆九十年代、八十年代的论文。显然，类型理论有很多变体。哪一个适合当代Coq？或者我应该认为“所有已知的东西都可以在 https://coq.inria.fr/refman/、https://sympa.inria.fr/sympa/arc/coq-club/1993-12/ 和标准库中找到。

（A） 你是否知道证明某些公理可以适当地添加到辅酶的论文或其他来源？ 这里的正确含义是扩展系统将是先前OR的保守扩展，将被视为安全加强。

（B）就我个人而言，我对这些公理感兴趣：

0） ex2sig（是否一致？

Axiom ex2sig : forall (A:Type) (P:A->Prop), @ex A P -> @sig A P.

1） 莱姆

2）功能延伸性

Axiom functional_extensionality_dep : forall {A} {B : A -> Type},
  forall (f g : forall x : A, B x),
  (forall x, f x = g x) -> f = g.

3） 选择

Theorem choice :
 forall (A B : Type) (R : A->B->Prop),
   (forall x : A, exists y : B, R x y) ->
    exists f : A->B, (forall x : A, R x (f x)).

4）“术语即类型”

Definition E := Type.
Axiom R : forall x : E, x -> E.  
Axiom R_inj : forall (x : E) (a b : x), R x a = R x b -> a = b.

5）证明-无关紧要

Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.

6) ...（你可以在评论中推荐你的公理）

例如马尔科夫原理

Parameter P:nat -> Prop.
Theorem M:((forall n,(P n \/ ~ (P n)))/\ ~(forall n, ~(P n))  -> exists n,P n).

但我们对马尔科夫的原理不是很感兴趣。 因为我们需要一些非常强大的经典理论和 LEM（所以马尔可夫原理被证明），以及一些最强形式的选择（这将意味着 LEM）、外延性等（我们还可以添加哪些公理？（顺便说一句，Coq中有许多选择：关系）

p.s. 在Coq中广泛使用“非计算”公理是否应被视为滥用它？（我认为不是，但我不确定。 添加公理后，我会失去 Coq 的哪些属性？（你可以说参考和/或意见）

P.P.S.这个问题很大，由许多相互关联的部分组成，因此欢迎每一个部分答案。