diff options
| author | krasimir <krasimir@chalmers.se> | 2010-03-15 10:47:00 +0000 |
|---|---|---|
| committer | krasimir <krasimir@chalmers.se> | 2010-03-15 10:47:00 +0000 |
| commit | aef1a1a5a35a403b3d32c3e3ad8923310a0624f0 (patch) | |
| tree | 3b34997b4dc3b8938371e95d8839e55c755139c1 /examples | |
| parent | 9f45bb0df10f8367bff0851da5fea3129a0512c0 (diff) | |
incomplete code for composition of functors
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/category-theory/Functor.gf | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/examples/category-theory/Functor.gf b/examples/category-theory/Functor.gf index 70ec1a940..e6df95b0f 100644 --- a/examples/category-theory/Functor.gf +++ b/examples/category-theory/Functor.gf @@ -8,5 +8,17 @@ 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 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) ? ;
+fun mapEqAr : ({c} : Category)
+ -> ({x,y} : El c)
+ -> ({f,g} : Arrow x y)
+ -> (func : Arrow x y -> Arrow x y)
+ -> EqAr f g
+ -> EqAr (func f) (func g) ;
+def mapEqAr {c} {x} {y} {f} {f} func (eqRefl {c} {x} {y} f) = eqRefl (func f) ;
+-}
}
\ No newline at end of file |