From 19851031e69d05e802eeabfe5db55e58583e1ba0 Mon Sep 17 00:00:00 2001 From: krasimir Date: Tue, 1 Jun 2010 06:03:19 +0000 Subject: [PATCH] cleanup the code for category theory --- examples/category-theory/Categories.gf | 53 ++++++++++--------- examples/category-theory/Functor.gf | 21 ++++---- .../category-theory/InitialAndTerminal.gf | 10 ++-- examples/category-theory/Morphisms.gf | 13 +++-- 4 files changed, 49 insertions(+), 48 deletions(-) diff --git a/examples/category-theory/Categories.gf b/examples/category-theory/Categories.gf index 6cc557d81..91a30c61b 100644 --- a/examples/category-theory/Categories.gf +++ b/examples/category-theory/Categories.gf @@ -7,7 +7,7 @@ abstract Categories = { fun dom : ({c} : Category) -> ({x,y} : El c) -> Arrow x y -> El c ; def dom {_} {x} {y} _ = x ; - + fun codom : ({c} : Category) -> ({x,y} : El c) -> Arrow x y -> El c ; def codom {_} {x} {y} _ = y ; @@ -24,15 +24,15 @@ abstract Categories = { -> ({a,b} : Arrow x y) -> EqAr a b -> EqAr b a ; - def eqSym {c} {x} {y} {a} {a} (eqRefl {c} {x} {y} a) = eqRefl a ; - + def eqSym (eqRefl a) = eqRefl a ; + fun eqTran : ({c} : Category) -> ({x,y} : El c) -> ({f,g,h} : Arrow x y) -> EqAr f g -> EqAr f h -> EqAr g h ; - def eqTran {c} {x} {y} {a} {a} {b} (eqRefl {c} {x} {y} a) eq = eq ; + def eqTran (eqRefl a) eq = eq ; fun eqCompL : ({c} : Category) -> ({x,y,z} : El c) @@ -40,7 +40,7 @@ abstract Categories = { -> (f : Arrow z y) -> EqAr g h -> EqAr (comp f g) (comp f h) ; - def eqCompL {c} {x} {y} {z} {g} {g} f (eqRefl {c} {x} {z} g) = eqRefl (comp f g) ; + def eqCompL f (eqRefl g) = eqRefl (comp f g) ; fun eqCompR : ({c} : Category) -> ({x,y,z} : El c) @@ -48,7 +48,7 @@ abstract Categories = { -> EqAr g h -> (f : Arrow x z) -> EqAr (comp g f) (comp h f) ; - def eqCompR {c} {x} {y} {z} {g} {g} (eqRefl {c} {z} {y} g) f = eqRefl (comp g f) ; + def eqCompR (eqRefl g) f = eqRefl (comp g f) ; fun eqIdL : ({c} : Category) -> ({x,y} : El c) @@ -75,17 +75,17 @@ abstract Categories = { -> ({x,y} : El c) -> (a : Arrow x y) -> Arrow {Op c} (opEl y) (opEl x) ; - def id {Op c} (opEl {c} x) = opAr (id x) ; - def comp {Op c} {opEl {c} x} {opEl {c} y} {opEl {c} z} (opAr {c} {y} {z} f) (opAr {c} {z} {x} g) = opAr (comp g f) ; - + def id (opEl x) = opAr (id x) ; + def comp (opAr f) (opAr g) = opAr (comp g f) ; + fun eqOp : ({c} : Category) -> ({x,y} : El c) -> ({f} : Arrow x y) -> ({g} : Arrow x y) -> EqAr f g -> EqAr (opAr f) (opAr g) ; - def eqOp {c} {x} {y} {f} {f} (eqRefl {c} {x} {y} f) = eqRefl (opAr f) ; - + def eqOp (eqRefl f) = eqRefl (opAr f) ; + data Slash : (c : Category) -> (x : El c) -> Category ; @@ -99,8 +99,8 @@ abstract Categories = { -> ({az} : Arrow z x) -> Arrow y z -> Arrow (slashEl x ay) (slashEl x az) ; - def id {Slash c x} (slashEl {c} x {y} a) = slashAr x {y} {y} {a} {a} (id y) ; - def comp {Slash c t} {slashEl {c} t {x} ax} {slashEl {c} t {y} ay} {slashEl {c} t {z} az} (slashAr {c} t {z} {y} {az} {ay} azy) (slashAr {c} t {x} {z} {ax} {az} axz) = slashAr t {x} {y} {ax} {ay} (comp azy axz) ; + def id (slashEl x {y} a) = slashAr x (id y) ; + def comp (slashAr t azy) (slashAr ~t axz) = slashAr t (comp azy axz) ; data CoSlash : (c : Category) -> (x : El c) @@ -115,8 +115,8 @@ abstract Categories = { -> ({az} : Arrow x z) -> Arrow z y -> Arrow (coslashEl x ay) (coslashEl x az) ; - def id {CoSlash c x} (coslashEl {c} x {y} a) = coslashAr x (id y) ; - def comp {CoSlash c t} {coslashEl {c} t {x} ax} {coslashEl {c} t {y} ay} {coslashEl {c} t {z} az} (coslashAr {c} t {z} {y} {az} {ay} ayz) (coslashAr {c} t {x} {z} {ax} {az} azx) = coslashAr t {x} {y} {ax} {ay} (comp azx ayz) ; + def id (coslashEl x {y} a) = coslashAr x (id y) ; + def comp (coslashAr t ayz) (coslashAr ~t azx) = coslashAr t (comp azx ayz) ; data Prod : (c1,c2 : Category) -> Category ; @@ -130,15 +130,15 @@ abstract Categories = { -> Arrow x1 y1 -> Arrow x2 y2 -> Arrow (prodEl x1 x2) (prodEl y1 y2) ; - def id {Prod c1 c2} (prodEl {c1} {c2} x1 x2) = prodAr (id x1) (id x2) ; - def comp {Prod c1 c2} {prodEl {c1} {c2} x1 x2} {prodEl {c1} {c2} y1 y2} {prodEl {c1} {c2} z1 z2} (prodAr {c1} {c2} {z1} {y1} {z2} {y2} f1 f2) (prodAr {c1} {c2} {x1} {z1} {x2} {z2} g1 g2) = prodAr {c1} {c2} {x1} {y1} {x2} {y2} (comp f1 g1) (comp f2 g2) ; - + def id (prodEl x1 x2) = prodAr (id x1) (id x2) ; + def comp (prodAr f1 f2) (prodAr g1 g2) = prodAr (comp f1 g1) (comp f2 g2) ; + fun fst : ({c1,c2} : Category) -> El (Prod c1 c2) -> El c1 ; - def fst {c1} {c2} (prodEl {c1} {c2} x1 _) = x1 ; + def fst (prodEl x1 _) = x1 ; fun snd : ({c1,c2} : Category) -> El (Prod c1 c2) -> El c2 ; - def snd {c1} {c2} (prodEl {c1} {c2} _ x2) = x2 ; - + def snd (prodEl _ x2) = x2 ; + data Sum : (c1,c2 : Category) -> Category ; sumLEl : ({c1,c2} : Category) @@ -155,10 +155,11 @@ abstract Categories = { -> ({x,y} : El c2) -> Arrow x y -> Arrow {Sum c1 c2} (sumREl x) (sumREl y) ; - def id {Sum c1 c2} (sumLEl {c1} {c2} x) = sumLAr (id x) ; - id {Sum c1 c2} (sumREl {c1} {c2} x) = sumRAr (id x) ; - comp {Sum c1 c2} {sumREl {c1} {c2} x} {sumREl {c1} {c2} y} {sumREl {c1} {c2} z} (sumRAr {c1} {c2} {z} {y} f) (sumRAr {c1} {c2} {x} {z} g) = sumRAr (comp f g) ; - comp {Sum c1 c2} {sumLEl {c1} {c2} x} {sumLEl {c1} {c2} y} {sumLEl {c1} {c2} z} (sumLAr {c1} {c2} {z} {y} f) (sumLAr {c1} {c2} {x} {z} g) = sumLAr (comp f g) ; + def id (sumLEl x) = sumLAr (id x) ; + id (sumREl x) = sumRAr (id x) ; -} \ No newline at end of file + comp (sumRAr f) (sumRAr g) = sumRAr (comp f g) ; + comp (sumLAr f) (sumLAr g) = sumLAr (comp f g) ; + +} diff --git a/examples/category-theory/Functor.gf b/examples/category-theory/Functor.gf index 5ad65bac4..2c638eab9 100644 --- a/examples/category-theory/Functor.gf +++ b/examples/category-theory/Functor.gf @@ -10,32 +10,31 @@ data functor : ({c1, c2} : Category) -> 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)) ; +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 (functor f032 f132 eqid32 eqcmp32) (functor 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 -> El c1 -> El c2 ; -def mapEl {c1} {c2} (functor {c1} {c2} f0 f1 _ _) = f0 ; -{- +def mapEl (functor f0 f1 _ _) = f0 ; + fun mapAr : ({c1, c2} : Category) -> ({x,y} : El c1) -> (f : Functor c1 c2) -> Arrow x y -> Arrow (mapEl f x) (mapEl f y) ; -def mapAr {c1} {c2} {x} {y} (functor {c1} {c2} f0 f1 _ _) = f1 {x} {y} ; --} -{- +def mapAr (functor f0 f1 _ _) = f1 ; + 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 +def mapEqAr func (eqRefl f) = eqRefl (func f) ; + +} diff --git a/examples/category-theory/InitialAndTerminal.gf b/examples/category-theory/InitialAndTerminal.gf index 856fc1788..ac665f856 100644 --- a/examples/category-theory/InitialAndTerminal.gf +++ b/examples/category-theory/InitialAndTerminal.gf @@ -11,13 +11,14 @@ fun initAr : ({c} : Category) -> Initial x -> (y : El c) -> Arrow x y ; -def initAr {c} {x} (initial {c} x f) y = f y ; - +-- def initAr {~c} {~x} (initial {c} x f) y = f y ; +{- fun initials2iso : ({c} : Category) -> ({x,y} : El c) -> (ix : Initial x) -> (iy : Initial y) -> Iso (initAr ix y) (initAr iy x) ; +-} -- def initials2iso = .. ; @@ -32,13 +33,14 @@ fun terminalAr : ({c} : Category) -> ({y} : El c) -> Terminal y -> Arrow x y ; -def terminalAr {c} x {y} (terminal {c} y f) = f x ; - +-- def terminalAr {c} x {~y} (terminal {~c} y f) = f x ; +{- fun terminals2iso : ({c} : Category) -> ({x,y} : El c) -> (tx : Terminal x) -> (ty : Terminal y) -> Iso (terminalAr x ty) (terminalAr y tx) ; + -} -- def terminals2iso = .. ; } \ No newline at end of file diff --git a/examples/category-theory/Morphisms.gf b/examples/category-theory/Morphisms.gf index e5f21c925..df40f5abe 100644 --- a/examples/category-theory/Morphisms.gf +++ b/examples/category-theory/Morphisms.gf @@ -16,15 +16,14 @@ fun isoOp : ({c} : Category) -> ({g} : Arrow y x) -> Iso f g -> Iso (opAr g) (opAr f) ; -def isoOp {c} {x} {y} {f} {g} (iso {c} {x} {y} f g id_fg id_gf) = - iso {Op c} (opAr g) (opAr f) (eqOp id_fg) (eqOp id_gf) ; +def isoOp (iso f g id_fg id_gf) = iso (opAr g) (opAr f) (eqOp id_fg) (eqOp id_gf) ; fun iso2mono : ({c} : Category) -> ({x,y} : El c) -> ({f} : Arrow x y) -> ({g} : Arrow y x) -> (Iso f g -> Mono f) ; -def iso2mono {c} {x} {y} {f} {g} (iso {c} {x} {y} f g id_fg id_gf) = +def iso2mono (iso f g id_fg id_gf) = mono f (\h,m,eq_fh_fm -> eqSym (eqTran (eqIdR m) -- h = m (eqTran (eqCompR id_gf m) -- id . m = h @@ -40,8 +39,9 @@ fun iso2epi : ({c} : Category) -> ({f} : Arrow x y) -> ({g} : Arrow y x) -> (Iso f g -> Epi f) ; -def iso2epi {c} {x} {y} {f} {g} (iso {c} {x} {y} f g id_fg id_gf) = - epi {c} {x} {y} f (\{z},h,m,eq_hf_mf -> + +def iso2epi (iso fff g id_fg id_gf) = + epi f (\h,m,eq_hf_mf -> eqSym (eqTran (eqIdL m) -- h = m (eqTran (eqCompL m id_fg) -- m . id = h (eqTran (eqSym (eqAssoc m f g)) -- m . (f . g) = h @@ -59,7 +59,6 @@ data mono : ({c} : Category) -> (({z} : El c) -> (h,m : Arrow z x) -> EqAr (comp f h) (comp f m) -> EqAr h m) -> Mono f ; - cat Epi ({c} : Category) ({x,y} : El c) (Arrow x y) ; data epi : ({c} : Category) @@ -68,4 +67,4 @@ data epi : ({c} : Category) -> (({z} : El c) -> (h,m : Arrow y z) -> EqAr (comp h f) (comp m f) -> EqAr h m) -> Epi f ; -} \ No newline at end of file +}