rewrite/Univs: Fix bug # 4498.

1 files changed, 24 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4498.v b/test-suite/bugs/closed/4498.v
new file mode 100644
index 000000000..ccdb2dddd
--- /dev/null
+++ b/test-suite/bugs/closed/4498.v
@@ -0,0 +1,24 @@
+Require Export Coq.Unicode.Utf8.
+Require Export Coq.Classes.Morphisms.
+Require Export Coq.Relations.Relation_Definitions.
+
+Set Universe Polymorphism.
+
+Reserved Notation "a ~> b" (at level 90, right associativity).
+
+Class Category := {
+  ob            : Type;
+  uhom          := Type : Type;
+  hom           : ob → ob → uhom where "a ~> b" := (hom a b);
+  compose       : ∀ {A B C}, (B ~> C) → (A ~> B) → (A ~> C);
+  equiv         : ∀ {A B}, relation (A ~> B);
+  is_equiv      : ∀ {A B}, @Equivalence (A ~> B) equiv;
+  comp_respects : ∀ {A B C},
+      Proper (@equiv B C ==> @equiv A B ==> @equiv A C) (@compose A B C);
+}.
+
+Require Export Coq.Setoids.Setoid.
+
+Add Parametric Morphism `{C : Category} {A B C} : (@compose _ A B C) with
+  signature equiv ==> equiv ==> equiv as compose_mor.
+Proof. apply comp_respects. Qed.
\ No newline at end of file