From 381a7a2f07f013f02df60ee345527df80c48bd84 Mon Sep 17 00:00:00 2001 From: krasimir Date: Mon, 15 Mar 2010 16:35:00 +0000 Subject: [PATCH] identity functor --- examples/category-theory/Functor.gf | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/examples/category-theory/Functor.gf b/examples/category-theory/Functor.gf index 58432a349..5ad65bac4 100644 --- a/examples/category-theory/Functor.gf +++ b/examples/category-theory/Functor.gf @@ -8,11 +8,13 @@ data functor : ({c1, c2} : Category) -> ((x : El c1) -> EqAr (f1 (id x)) (id (f0 x))) -> (({x,y,z} : El c1) -> (f : Arrow x z) -> (g : Arrow z y) -> EqAr (f1 (comp g f)) (comp (f1 g) (f1 f))) -> Functor c1 c2 ; -{- + +fun idF : (c : Category) -> Functor c c ; +-- def idF c = functor (\x->x) (\f->f) (\x -> eqRefl (id x)) (\f,g -> eqRefl (comp g f)) ; + fun compF : ({c1,c2,c3} : Category) -> Functor c3 c2 -> Functor c1 c3 -> Functor c1 c2 ; -def compF {c1} {c2} {c3} (functor {c3} {c2} f032 f132 eqid32 eqcmp32) (functor {c1} {c3} f013 f113 eqid13 eqcmp13) = - functor (\x -> f032 (f013 x)) (\x -> f132 (f113 x)) (\x -> mapEqAr (f132 {?} {?}) eqid13) ? ; --} +-- def compF {c1} {c2} {c3} (functor {c3} {c2} f032 f132 eqid32 eqcmp32) (functor {c1} {c3} f013 f113 eqid13 eqcmp13) = +-- functor (\x -> f032 (f013 x)) (\x -> f132 (f113 x)) (\x -> mapEqAr (f132 {?} {?}) eqid13) ? ; fun mapEl : ({c1, c2} : Category) -> Functor c1 c2