From e11f4b59fe2b8d87f6a324ae18189efe4956254a Mon Sep 17 00:00:00 2001
From: John Wiegley <johnw@newartisans.com>
Date: Tue, 26 Mar 2024 14:30:33 -0700
Subject: [PATCH] Notational simplifications in Cayley.v

---
 Construction/Cayley.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Construction/Cayley.v b/Construction/Cayley.v
index cb3d0f33..c7fd2881 100644
--- a/Construction/Cayley.v
+++ b/Construction/Cayley.v
@@ -19,7 +19,7 @@ Program Instance Cayley : Category := {
   hom     := fun x y =>
     { f : ∀ r, (y ~> r) → (x ~> r)
     & Proper (forall_relation (fun _ => respectful equiv equiv)) f ∧
-      ∀ r k, f r k ≈ k ∘ f _ id[y] };
+      ∀ (r : C) (k : y ~> r), f r k ≈ k ∘ f _ id };
   homset  := fun x y => {| equiv := fun f g => ∀ r k, `1 f r k ≈ `1 g r k |};
   id      := fun _ => (fun _ => Datatypes.id; _);
   compose := fun x y z f g  => (fun r k => `1 g r (`1 f r k); _)
@@ -67,7 +67,7 @@ Defined.
 
 Program Instance From_Cayley : Cayley ⟶ C := {
   fobj := fun x => x;
-  fmap := fun x y f => `1 f y (@id C y);
+  fmap := fun _ y f => `1 f y (@id C y);
 }.
 
 Context `{Cayley}.