diff options
Diffstat (limited to 'theories/Classes/SetoidClass.v')
| -rw-r--r-- | theories/Classes/SetoidClass.v | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index c5befaa115..f61b4a4159 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -223,17 +223,21 @@ Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => (** We redefine respect for binary and ternary morphims because we cannot get a satisfying instance of [Setoid (a -> b)] from some arbitrary domain and codomain setoids. We can define it on respectful Coq functions though, see [arrow_setoid] above. *) -Definition binary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, Setoid c eqc ] (m : a -> b -> c) : Prop := +Definition binary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, Setoid c eqc ] + (m : a -> b -> c) : Prop := forall x y, eqa x y -> forall z w, eqb z w -> eqc (m x z) (m y w). -Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc ] => BinaryMorphism (m : a -> b -> c) := +Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc ] => + BinaryMorphism (m : a -> b -> c) := respect2 : binary_respectful m. -Definition ternary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, Setoid d eqd ] (m : a -> b -> c -> d) : Prop := +Definition ternary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, Setoid d eqd ] + (m : a -> b -> c -> d) : Prop := forall x y, eqa x y -> forall z w, eqb z w -> forall u v, eqc u v -> eqd (m x z u) (m y w v). -Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, sd : Setoid d eqd ] => TernaryMorphism (m : a -> b -> c -> d) := +Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, sd : Setoid d eqd ] => + TernaryMorphism (m : a -> b -> c -> d) := respect3 : ternary_respectful m. (** Definition of the usual morphisms in [Prop]. *) |