From 43bbaeee02ed047d80beb465e8a00d02f97130c4 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Wed, 9 Jun 2021 10:57:10 +0900
Subject: [PATCH] fixes #50

---
 hierarchy.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/hierarchy.v b/hierarchy.v
index 2ff4fa04..75f6a036 100644
--- a/hierarchy.v
+++ b/hierarchy.v
@@ -371,7 +371,7 @@ Definition left_zero (f : forall A, M A) :=
 Definition right_zero (f : forall A, M A) :=
   forall (A B : UU0) (g : M B), g >>= (fun _ => f A) = f A.
 
-Definition left_neutral (r : FId ~> M) :=
+Definition left_neutral (r : forall A : UU0, A -> M A) :=
   forall (A B : UU0) (a : A) (f : A -> M B), r _ a >>= f = f a.
 
 Definition right_neutral (r : forall A : UU0, A -> M A) :=