From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Thu, 1 Dec 2016 14:42:30 +0000 (+0100)
Subject: add a comment to category
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=f66ed8d4cf4cd9caa26351e27185329ca74c4cc5;p=cubicaltt.git

add a comment to category
---

diff --git a/examples/category.ctt b/examples/category.ctt
index ed6c5d1..71ff7f3 100644
--- 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))