GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-05-21 09:02:50 -06:00
Code Issues Packages Projects Releases Wiki Activity

cleanup the code for category theory

Browse Source
This commit is contained in:
krasimir
2010-06-01 06:03:19 +00:00
parent 7f3cfb3e95
commit 19851031e6
4 changed files with 49 additions and 48 deletions
Download Patch File Download Diff File Expand all files Collapse all files

39
examples/category-theory/Categories.gf
View File

@@ -24,7 +24,7 @@ abstract Categories = {
-> ({a,b} : Arrow x y) -> ({a,b} : Arrow x y)
-> EqAr a b -> EqAr a b
-> EqAr b a ; -> 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) fun eqTran : ({c} : Category)
-> ({x,y} : El c) -> ({x,y} : El c)
@@ -32,7 +32,7 @@ abstract Categories = {
-> EqAr f g -> EqAr f g
-> EqAr f h -> EqAr f h
-> EqAr g 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) fun eqCompL : ({c} : Category)
-> ({x,y,z} : El c) -> ({x,y,z} : El c)
@@ -40,7 +40,7 @@ abstract Categories = {
-> (f : Arrow z y) -> (f : Arrow z y)
-> EqAr g h -> EqAr g h
-> EqAr (comp f g) (comp f 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) fun eqCompR : ({c} : Category)
-> ({x,y,z} : El c) -> ({x,y,z} : El c)
@@ -48,7 +48,7 @@ abstract Categories = {
-> EqAr g h -> EqAr g h
-> (f : Arrow x z) -> (f : Arrow x z)
-> EqAr (comp g f) (comp h f) ; -> 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) fun eqIdL : ({c} : Category)
-> ({x,y} : El c) -> ({x,y} : El c)
@@ -75,8 +75,8 @@ abstract Categories = {
-> ({x,y} : El c) -> ({x,y} : El c)
-> (a : Arrow x y) -> (a : Arrow x y)
-> Arrow {Op c} (opEl y) (opEl x) ; -> Arrow {Op c} (opEl y) (opEl x) ;
def id {Op c} (opEl {c} x) = opAr (id x) ; def id (opEl 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 comp (opAr f) (opAr g) = opAr (comp g f) ;
fun eqOp : ({c} : Category) fun eqOp : ({c} : Category)
-> ({x,y} : El c) -> ({x,y} : El c)
@@ -84,7 +84,7 @@ abstract Categories = {
-> ({g} : Arrow x y) -> ({g} : Arrow x y)
-> EqAr f g -> EqAr f g
-> EqAr (opAr f) (opAr 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) data Slash : (c : Category)
-> (x : El c) -> (x : El c)
@@ -99,8 +99,8 @@ abstract Categories = {
-> ({az} : Arrow z x) -> ({az} : Arrow z x)
-> Arrow y z -> Arrow y z
-> Arrow (slashEl x ay) (slashEl x az) ; -> 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 id (slashEl x {y} a) = slashAr x (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 comp (slashAr t azy) (slashAr ~t axz) = slashAr t (comp azy axz) ;
data CoSlash : (c : Category) data CoSlash : (c : Category)
-> (x : El c) -> (x : El c)
@@ -115,8 +115,8 @@ abstract Categories = {
-> ({az} : Arrow x z) -> ({az} : Arrow x z)
-> Arrow z y -> Arrow z y
-> Arrow (coslashEl x ay) (coslashEl x az) ; -> Arrow (coslashEl x ay) (coslashEl x az) ;
def id {CoSlash c x} (coslashEl {c} x {y} a) = coslashAr x (id y) ; def id (coslashEl 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 comp (coslashAr t ayz) (coslashAr ~t azx) = coslashAr t (comp azx ayz) ;
data Prod : (c1,c2 : Category) data Prod : (c1,c2 : Category)
-> Category ; -> Category ;
@@ -130,14 +130,14 @@ abstract Categories = {
-> Arrow x1 y1 -> Arrow x1 y1
-> Arrow x2 y2 -> Arrow x2 y2
-> Arrow (prodEl x1 x2) (prodEl y1 y2) ; -> Arrow (prodEl x1 x2) (prodEl y1 y2) ;
def id {Prod c1 c2} (prodEl {c1} {c2} x1 x2) = prodAr (id x1) (id x2) ; def id (prodEl 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 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 ; 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 ; 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) data Sum : (c1,c2 : Category)
-> Category ; -> Category ;
@@ -155,10 +155,11 @@ abstract Categories = {
-> ({x,y} : El c2) -> ({x,y} : El c2)
-> Arrow x y -> Arrow x y
-> Arrow {Sum c1 c2} (sumREl x) (sumREl 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) ; def id (sumLEl x) = sumLAr (id x) ;
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) ; id (sumREl x) = sumRAr (id x) ;
comp (sumRAr f) (sumRAr g) = sumRAr (comp f g) ;
comp (sumLAr f) (sumLAr g) = sumLAr (comp f g) ;
} }

19
examples/category-theory/Functor.gf
View File

@@ -10,32 +10,31 @@ data functor : ({c1, c2} : Category)
-> Functor c1 c2 ; -> Functor c1 c2 ;
fun idF : (c : Category) -> Functor c c ; 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 ; 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) = 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) ? ; functor (\x -> f032 (f013 x)) (\x -> f132 (f113 x)) (\x -> mapEqAr f132 eqid13) ? ;
fun mapEl : ({c1, c2} : Category) fun mapEl : ({c1, c2} : Category)
-> Functor c1 c2 -> Functor c1 c2
-> El c1 -> El c1
-> El c2 ; -> El c2 ;
def mapEl {c1} {c2} (functor {c1} {c2} f0 f1 _ _) = f0 ; def mapEl (functor f0 f1 _ _) = f0 ;
{-
fun mapAr : ({c1, c2} : Category) fun mapAr : ({c1, c2} : Category)
-> ({x,y} : El c1) -> ({x,y} : El c1)
-> (f : Functor c1 c2) -> (f : Functor c1 c2)
-> Arrow x y -> Arrow x y
-> Arrow (mapEl f x) (mapEl f 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) fun mapEqAr : ({c} : Category)
-> ({x,y} : El c) -> ({x,y} : El c)
-> ({f,g} : Arrow x y) -> ({f,g} : Arrow x y)
-> (func : Arrow x y -> Arrow x y) -> (func : Arrow x y -> Arrow x y)
-> EqAr f g -> EqAr f g
-> EqAr (func f) (func g) ; -> EqAr (func f) (func g) ;
def mapEqAr {c} {x} {y} {f} {f} func (eqRefl {c} {x} {y} f) = eqRefl (func f) ; def mapEqAr func (eqRefl f) = eqRefl (func f) ;
-}
} }

10
examples/category-theory/InitialAndTerminal.gf
View File

@@ -11,13 +11,14 @@ fun initAr : ({c} : Category)
-> Initial x -> Initial x
-> (y : El c) -> (y : El c)
-> Arrow x y ; -> 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) fun initials2iso : ({c} : Category)
-> ({x,y} : El c) -> ({x,y} : El c)
-> (ix : Initial x) -> (ix : Initial x)
-> (iy : Initial y) -> (iy : Initial y)
-> Iso (initAr ix y) (initAr iy x) ; -> Iso (initAr ix y) (initAr iy x) ;
-}
-- def initials2iso = .. ; -- def initials2iso = .. ;
@@ -32,13 +33,14 @@ fun terminalAr : ({c} : Category)
-> ({y} : El c) -> ({y} : El c)
-> Terminal y -> Terminal y
-> Arrow x 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) fun terminals2iso : ({c} : Category)
-> ({x,y} : El c) -> ({x,y} : El c)
-> (tx : Terminal x) -> (tx : Terminal x)
-> (ty : Terminal y) -> (ty : Terminal y)
-> Iso (terminalAr x ty) (terminalAr y tx) ; -> Iso (terminalAr x ty) (terminalAr y tx) ;
-}
-- def terminals2iso = .. ; -- def terminals2iso = .. ;
} }

11
examples/category-theory/Morphisms.gf
View File

@@ -16,15 +16,14 @@ fun isoOp : ({c} : Category)
-> ({g} : Arrow y x) -> ({g} : Arrow y x)
-> Iso f g -> Iso f g
-> Iso (opAr g) (opAr f) ; -> Iso (opAr g) (opAr f) ;
def isoOp {c} {x} {y} {f} {g} (iso {c} {x} {y} f g id_fg id_gf) = def isoOp (iso f g id_fg id_gf) = iso (opAr g) (opAr f) (eqOp id_fg) (eqOp id_gf) ;
iso {Op c} (opAr g) (opAr f) (eqOp id_fg) (eqOp id_gf) ;
fun iso2mono : ({c} : Category) fun iso2mono : ({c} : Category)
-> ({x,y} : El c) -> ({x,y} : El c)
-> ({f} : Arrow x y) -> ({f} : Arrow x y)
-> ({g} : Arrow y x) -> ({g} : Arrow y x)
-> (Iso f g -> Mono f) ; -> (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 -> mono f (\h,m,eq_fh_fm ->
eqSym (eqTran (eqIdR m) -- h = m eqSym (eqTran (eqIdR m) -- h = m
(eqTran (eqCompR id_gf m) -- id . m = h (eqTran (eqCompR id_gf m) -- id . m = h
@@ -40,8 +39,9 @@ fun iso2epi : ({c} : Category)
-> ({f} : Arrow x y) -> ({f} : Arrow x y)
-> ({g} : Arrow y x) -> ({g} : Arrow y x)
-> (Iso f g -> Epi f) ; -> (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 eqSym (eqTran (eqIdL m) -- h = m
(eqTran (eqCompL m id_fg) -- m . id = h (eqTran (eqCompL m id_fg) -- m . id = h
(eqTran (eqSym (eqAssoc m f g)) -- m . (f . g) = 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) -> (({z} : El c) -> (h,m : Arrow z x) -> EqAr (comp f h) (comp f m) -> EqAr h m)
-> Mono f ; -> Mono f ;
cat Epi ({c} : Category) ({x,y} : El c) (Arrow x y) ; cat Epi ({c} : Category) ({x,y} : El c) (Arrow x y) ;
data epi : ({c} : Category) data epi : ({c} : Category)