Variable I : Type. Variable I_eq :I -> I -> Prop. Variable I_eq_equiv : Setoid_Theory I I_eq.
(* Add Relation I I_eq reflexivity proved by I_eq_equiv.(Seq_refl I I_eq) symmetry proved by I_eq_equiv.(Seq_sym I I_eq) transitivity proved by I_eq_equiv.(Seq_trans I I_eq)
as I_eq_relation. *)
Add Parametric Relation : I I_eq reflexivity proved by I_eq_equiv.(@Equivalence_Reflexive _ _) symmetry proved by I_eq_equiv.(@Equivalence_Symmetric _ _)
transitivity proved by I_eq_equiv.(@Equivalence_Transitive _ _) as I_with_eq.
Variable F : I -> Type. Variable F_morphism : forall i j, I_eq i j -> F i = F j.
Add Morphism F with signature I_eq ==> (@eq _) as F_morphism2. Admitted.
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
