added requested comment

agda · Sep 2, 2024 · 96ca966 · 96ca966
1 parent cc3264c
commit 96ca966
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/Cubical/Categories/Instances/Sets.agda b/Cubical/Categories/Instances/Sets.agda
@@ -152,6 +152,11 @@ univProp (completeSET J D) c cc =
 
 module _ {ℓ} where
 
+-- While pullbacks can be obtained from limits
+-- (using `completeSET` & `LimitsOfShapeCospanCat→Pullbacks` from `Cubical.Categories.Limits.Pullback`),
+-- this direct construction can be more convenient when only pullbacks are needed.
+-- It also has better behavior in terms of inferring implicit arguments
+
  open Pullback
 
  PullbacksSET : Pullbacks (SET ℓ)