From 8936d95d741db7a66db329cd77adda7b09193e70 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 19 Nov 2017 22:36:02 +0100 Subject: [PATCH] Explicit uses of a scope. --- theories/Categories/Comma/ProjectionFunctors.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/Categories/Comma/ProjectionFunctors.v b/theories/Categories/Comma/ProjectionFunctors.v index 0e698e1440c..9a0022453a3 100644 --- a/theories/Categories/Comma/ProjectionFunctors.v +++ b/theories/Categories/Comma/ProjectionFunctors.v @@ -44,7 +44,7 @@ Section comma. Definition comma_category_projection_functor_object_of (ST : object ((A -> C)^op * (B -> C))) - : Cat / !((A * B; PAB) : Cat). + : Cat / !(((A * B)%category; PAB) : Cat). Proof. exists (Datatypes.fst ST / Datatypes.snd ST; P_comma _ _) (center _). exact (comma_category_projection (Datatypes.fst ST) (Datatypes.snd ST)). @@ -52,7 +52,7 @@ Section comma. Definition comma_category_projection_functor_morphism_of s d (m : morphism ((A -> C)^op * (B -> C)) s d) - : morphism (Cat / !((A * B; PAB) : Cat)) + : morphism (Cat / !(((A * B)%category; PAB) : Cat)) (comma_category_projection_functor_object_of s) (comma_category_projection_functor_object_of d). Proof. @@ -120,9 +120,9 @@ Section comma. Definition comma_category_projection_functor : Functor ((A -> C)^op * (B -> C)) - (Cat / !((A * B; PAB) : Cat)) + (Cat / !(((A * B)%category; PAB) : Cat)) := Build_Functor ((A -> C)^op * (B -> C)) - (Cat / !((A * B; PAB) : Cat)) + (Cat / !(((A * B)%category; PAB) : Cat)) comma_category_projection_functor_object_of comma_category_projection_functor_morphism_of comma_category_projection_functor_composition_of