add a comment to category

diff --git a/examples/category.ctt b/examples/category.ctt
index ed6c5d1532b5e84917d8f7d253a450aff67ca44e..71ff7f3d3bfcbd55b68e005653b8508b68109017 100644 (file)
--- a/examples/category.ctt
+++ b/examples/category.ctt
@@ -404,6 +404,7 @@ opaque sip
 -- Functors
 --
 
+-- TODO: define as functor_data and isFunctor
 functor (A B : precategory) : U
   = (Fob : cA A -> cA B)
   * (Fmor : (x y : cA A) -> cH A x y -> cH B (Fob x) (Fob y))