some comments in the code for category theory

1 files changed, 12 insertions, 7 deletions

diff --git a/examples/category-theory/Adjoints.gf b/examples/category-theory/Adjoints.gf
index cb4c8c6c0..b4987228d 100644
--- a/examples/category-theory/Adjoints.gf
+++ b/examples/category-theory/Adjoints.gf
@@ -1,11 +1,16 @@
 abstract Adjoints = NaturalTransform ** {

 

-cat Adjoints ({c1,c2} : Category) (Functor c1 c2) (Functor c2 c1) ;

+  ----------------------------------------------------------

+  -- Adjoint functors - pair of functors such that

+  -- there is a natural transformation from the identity

+  -- functor to the composition of the functors.

 

-data adjoints : ({c1,c2} : Category)

-              -> (f : Functor c1 c2)

-              -> (g : Functor c2 c1)

-              -> NT (idF c1) (compF g f)

-              -> Adjoints f g ;

+  cat Adjoints ({c1,c2} : Category) (Functor c1 c2) (Functor c2 c1) ;

 

-}
\ No newline at end of file
+  data adjoints : ({c1,c2} : Category)

+                -> (f : Functor c1 c2)

+                -> (g : Functor c2 c1)

+                -> NT (idF c1) (compF g f)

+                -> Adjoints f g ;

+

+}