msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

El -> Obj in category theory

Browse Source
This commit is contained in:
krasimir
2010-06-01 06:12:30 +00:00
parent 19851031e6
commit 5e0d04d0f5
6 changed files with 106 additions and 106 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -1,33 +1,33 @@
abstract Categories = {
cat Category ;
El Category ;
Arrow ({c} : Category) (El c) (El c) ;
EqAr ({c} : Category) ({x,y} : El c) (f,g : Arrow x y) ;
Obj Category ;
Arrow ({c} : Category) (Obj c) (Obj c) ;
EqAr ({c} : Category) ({x,y} : Obj c) (f,g : Arrow x y) ;
fun dom : ({c} : Category) -> ({x,y} : El c) -> Arrow x y -> El c ;
fun dom : ({c} : Category) -> ({x,y} : Obj c) -> Arrow x y -> Obj c ;
def dom {_} {x} {y} _ = x ;
fun codom : ({c} : Category) -> ({x,y} : El c) -> Arrow x y -> El c ;
fun codom : ({c} : Category) -> ({x,y} : Obj c) -> Arrow x y -> Obj c ;
def codom {_} {x} {y} _ = y ;
fun id : ({c} : Category) -> (x : El c) -> Arrow x x ;
fun id : ({c} : Category) -> (x : Obj c) -> Arrow x x ;
fun comp : ({c} : Category) -> ({x,y,z} : El c) -> Arrow z y -> Arrow x z -> Arrow x y ;
fun comp : ({c} : Category) -> ({x,y,z} : Obj c) -> Arrow z y -> Arrow x z -> Arrow x y ;
data eqRefl : ({c} : Category)
-> ({x,y} : El c)
-> ({x,y} : Obj c)
-> (a : Arrow x y)
-> EqAr a a ;
fun eqSym : ({c} : Category)
-> ({x,y} : El c)
-> ({x,y} : Obj c)
-> ({a,b} : Arrow x y)
-> EqAr a b
-> EqAr b a ;
def eqSym (eqRefl a) = eqRefl a ;
fun eqTran : ({c} : Category)
-> ({x,y} : El c)
-> ({x,y} : Obj c)
-> ({f,g,h} : Arrow x y)
-> EqAr f g
-> EqAr f h
@@ -35,7 +35,7 @@ abstract Categories = {
def eqTran (eqRefl a) eq = eq ;
fun eqCompL : ({c} : Category)
-> ({x,y,z} : El c)
-> ({x,y,z} : Obj c)
-> ({g,h} : Arrow x z)
-> (f : Arrow z y)
-> EqAr g h
@@ -43,7 +43,7 @@ abstract Categories = {
def eqCompL f (eqRefl g) = eqRefl (comp f g) ;
fun eqCompR : ({c} : Category)
-> ({x,y,z} : El c)
-> ({x,y,z} : Obj c)
-> ({g,h} : Arrow z y)
-> EqAr g h
-> (f : Arrow x z)
@@ -51,16 +51,16 @@ abstract Categories = {
def eqCompR (eqRefl g) f = eqRefl (comp g f) ;
fun eqIdL : ({c} : Category)
-> ({x,y} : El c)
-> ({x,y} : Obj c)
-> (a : Arrow x y)
-> EqAr (comp a (id x)) a ;
eqIdR : ({c} : Category)
-> ({x,y} : El c)
-> ({x,y} : Obj c)
-> (a : Arrow x y)
-> EqAr (comp (id y) a) a ;
fun eqAssoc : ({c} : Category)
-> ({w,x,y,z} : El c)
-> ({w,x,y,z} : Obj c)
-> (f : Arrow w y)
-> (g : Arrow z w)
-> (h : Arrow x z)
@@ -68,18 +68,18 @@ abstract Categories = {
data Op : (c : Category)
-> Category ;
opEl : ({c} : Category)
-> (x : El c)
-> El (Op c) ;
opObj: ({c} : Category)
-> (x : Obj c)
-> Obj (Op c) ;
opAr : ({c} : Category)
-> ({x,y} : El c)
-> ({x,y} : Obj c)
-> (a : Arrow x y)
-> Arrow {Op c} (opEl y) (opEl x) ;
def id (opEl x) = opAr (id x) ;
-> Arrow {Op c} (opObj y) (opObj x) ;
def id (opObj x) = opAr (id x) ;
def comp (opAr f) (opAr g) = opAr (comp g f) ;
fun eqOp : ({c} : Category)
-> ({x,y} : El c)
-> ({x,y} : Obj c)
-> ({f} : Arrow x y)
-> ({g} : Arrow x y)
-> EqAr f g
@@ -87,77 +87,77 @@ abstract Categories = {
def eqOp (eqRefl f) = eqRefl (opAr f) ;
data Slash : (c : Category)
-> (x : El c)
-> (x : Obj c)
-> Category ;
slashEl : ({c} : Category)
-> (x,{y} : El c)
slashObj : ({c} : Category)
-> (x,{y} : Obj c)
-> Arrow y x
-> El (Slash c x) ;
-> Obj (Slash c x) ;
slashAr : ({c} : Category)
-> (x,{y,z} : El c)
-> (x,{y,z} : Obj c)
-> ({ay} : Arrow y x)
-> ({az} : Arrow z x)
-> Arrow y z
-> Arrow (slashEl x ay) (slashEl x az) ;
def id (slashEl x {y} a) = slashAr x (id y) ;
-> Arrow (slashObj x ay) (slashObj x az) ;
def id (slashObj 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)
-> (x : Obj c)
-> Category ;
coslashEl : ({c} : Category)
-> (x,{y} : El c)
coslashObj: ({c} : Category)
-> (x,{y} : Obj c)
-> Arrow x y
-> El (CoSlash c x) ;
-> Obj (CoSlash c x) ;
coslashAr : ({c} : Category)
-> (x,{y,z} : El c)
-> (x,{y,z} : Obj c)
-> ({ay} : Arrow x y)
-> ({az} : Arrow x z)
-> Arrow z y
-> Arrow (coslashEl x ay) (coslashEl x az) ;
def id (coslashEl x {y} a) = coslashAr x (id y) ;
-> Arrow (coslashObj x ay) (coslashObj x az) ;
def id (coslashObj 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 ;
prodEl : ({c1,c2} : Category)
-> El c1
-> El c2
-> El (Prod c1 c2) ;
prodObj: ({c1,c2} : Category)
-> Obj c1
-> Obj c2
-> Obj (Prod c1 c2) ;
prodAr : ({c1,c2} : Category)
-> ({x1,y1} : El c1)
-> ({x2,y2} : El c2)
-> ({x1,y1} : Obj c1)
-> ({x2,y2} : Obj c2)
-> Arrow x1 y1
-> Arrow x2 y2
-> Arrow (prodEl x1 x2) (prodEl y1 y2) ;
def id (prodEl x1 x2) = prodAr (id x1) (id x2) ;
-> Arrow (prodObj x1 x2) (prodObj y1 y2) ;
def id (prodObj 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 (prodEl x1 _) = x1 ;
fun fst : ({c1,c2} : Category) -> Obj (Prod c1 c2) -> Obj c1 ;
def fst (prodObj x1 _) = x1 ;
fun snd : ({c1,c2} : Category) -> El (Prod c1 c2) -> El c2 ;
def snd (prodEl _ x2) = x2 ;
fun snd : ({c1,c2} : Category) -> Obj (Prod c1 c2) -> Obj c2 ;
def snd (prodObj _ x2) = x2 ;
data Sum : (c1,c2 : Category)
-> Category ;
sumLEl : ({c1,c2} : Category)
-> El c1
-> El (Sum c1 c2) ;
sumREl : ({c1,c2} : Category)
-> El c2
-> El (Sum c1 c2) ;
sumLObj: ({c1,c2} : Category)
-> Obj c1
-> Obj (Sum c1 c2) ;
sumRObj: ({c1,c2} : Category)
-> Obj c2
-> Obj (Sum c1 c2) ;
sumLAr : ({c1,c2} : Category)
-> ({x,y} : El c1)
-> ({x,y} : Obj c1)
-> Arrow x y
-> Arrow {Sum c1 c2} (sumLEl x) (sumLEl y) ;
-> Arrow {Sum c1 c2} (sumLObj x) (sumLObj y) ;
sumRAr : ({c1,c2} : Category)
-> ({x,y} : El c2)
-> ({x,y} : Obj c2)
-> Arrow x y
-> Arrow {Sum c1 c2} (sumREl x) (sumREl y) ;
-> Arrow {Sum c1 c2} (sumRObj x) (sumRObj y) ;
def id (sumLEl x) = sumLAr (id x) ;
id (sumREl x) = sumRAr (id x) ;
def id (sumLObj x) = sumLAr (id x) ;
id (sumRObj x) = sumRAr (id x) ;
comp (sumRAr f) (sumRAr g) = sumRAr (comp f g) ;
comp (sumLAr f) (sumLAr g) = sumLAr (comp f g) ;

18
examples/category-theory/Equalizer.gf
View File

@@ -1,49 +1,49 @@
abstract Equalizer = Morphisms ** {
cat Equalizer ({c} : Category) ({x,y,z} : El c) (f,g : Arrow x y) (e : Arrow z x) ;
cat Equalizer ({c} : Category) ({x,y,z} : Obj c) (f,g : Arrow x y) (e : Arrow z x) ;
data equalizer : ({c} : Category)
-> ({x,y,z} : El c)
-> ({x,y,z} : Obj c)
-> (f,g : Arrow x y)
-> (e : Arrow z x)
-> EqAr (comp f e) (comp g e)
-> Equalizer f g e ;
fun idEqualizer : ({c} : Category)
-> ({x,y} : El c)
-> ({x,y} : Obj c)
-> (f : Arrow x y)
-> Equalizer f f (id x) ;
def idEqualizer {c} {x} {y} f = equalizer f f (id x) (eqCompL f (eqRefl (id x))) ;
fun equalizer2mono : ({c} : Category)
-> ({x,y,z} : El c)
-> ({x,y,z} : Obj c)
-> (f,g : Arrow x y)
-> (e : Arrow z x)
-> Equalizer f g e
-> Mono e ;
-- def equalizer2mono = ...
cat CoEqualizer ({c} : Category) ({x,y,z} : El c) (e : Arrow y z) (f,g : Arrow x y) ;
cat CoEqualizer ({c} : Category) ({x,y,z} : Obj c) (e : Arrow y z) (f,g : Arrow x y) ;
data coequalizer : ({c} : Category)
-> ({x,y,z} : El c)
-> ({x,y,z} : Obj c)
-> (e : Arrow y z)
-> (f,g : Arrow x y)
-> EqAr (comp e f) (comp e g)
-> CoEqualizer e f g ;
fun idCoEqualizer : ({c} : Category)
-> ({x,y} : El c)
-> ({x,y} : Obj c)
-> (f : Arrow x y)
-> CoEqualizer (id y) f f ;
def idCoEqualizer {c} {x} {y} f = coequalizer (id y) f f (eqCompR (eqRefl (id y)) f) ;
fun coequalizer2epi : ({c} : Category)
-> ({x,y,z} : El c)
-> ({x,y,z} : Obj c)
-> ({e} : Arrow y z)
-> ({f,g} : Arrow x y)
-> CoEqualizer e f g
-> Epi e ;
-- def coequalizer2epi = ...
}
}

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

@@ -3,10 +3,10 @@ abstract Functor = Categories ** {
cat Functor (c1, c2 : Category) ;
data functor : ({c1, c2} : Category)
-> (f0 : El c1 -> El c2)
-> (f1 : ({x,y} : El c1) -> Arrow x y -> Arrow (f0 x) (f0 y))
-> ((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)))
-> (f0 : Obj c1 -> Obj c2)
-> (f1 : ({x,y} : Obj c1) -> Arrow x y -> Arrow (f0 x) (f0 y))
-> ((x : Obj c1) -> EqAr (f1 (id x)) (id (f0 x)))
-> (({x,y,z} : Obj 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 ;
@@ -16,21 +16,21 @@ fun compF : ({c1,c2,c3} : Category) -> Functor c3 c2 -> Functor c1 c3 -> Functor
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)
fun mapObj : ({c1, c2} : Category)
-> Functor c1 c2
-> El c1
-> El c2 ;
def mapEl (functor f0 f1 _ _) = f0 ;
-> Obj c1
-> Obj c2 ;
def mapObj (functor f0 f1 _ _) = f0 ;
fun mapAr : ({c1, c2} : Category)
-> ({x,y} : El c1)
-> ({x,y} : Obj c1)
-> (f : Functor c1 c2)
-> Arrow x y
-> Arrow (mapEl f x) (mapEl f y) ;
-> Arrow (mapObj f x) (mapObj f y) ;
def mapAr (functor f0 f1 _ _) = f1 ;
fun mapEqAr : ({c} : Category)
-> ({x,y} : El c)
-> ({x,y} : Obj c)
-> ({f,g} : Arrow x y)
-> (func : Arrow x y -> Arrow x y)
-> EqAr f g

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

@@ -1,20 +1,20 @@
abstract InitialAndTerminal = Morphisms ** {
cat Initial ({c} : Category) (El c) ;
cat Initial ({c} : Category) (Obj c) ;
data initial : ({c} : Category)
-> (x : El c)
-> ((y : El c) -> Arrow x y)
-> (x : Obj c)
-> ((y : Obj c) -> Arrow x y)
-> Initial x ;
fun initAr : ({c} : Category)
-> ({x} : El c)
-> ({x} : Obj c)
-> Initial x
-> (y : El c)
-> (y : Obj c)
-> Arrow x y ;
-- def initAr {~c} {~x} (initial {c} x f) y = f y ;
{-
fun initials2iso : ({c} : Category)
-> ({x,y} : El c)
-> ({x,y} : Obj c)
-> (ix : Initial x)
-> (iy : Initial y)
-> Iso (initAr ix y) (initAr iy x) ;
@@ -22,25 +22,25 @@ fun initials2iso : ({c} : Category)
-- def initials2iso = .. ;
cat Terminal ({c} : Category) (El c) ;
cat Terminal ({c} : Category) (Obj c) ;
data terminal : ({c} : Category)
-> (y : El c)
-> ((x : El c) -> Arrow x y)
-> (y : Obj c)
-> ((x : Obj c) -> Arrow x y)
-> Terminal y ;
fun terminalAr : ({c} : Category)
-> (x : El c)
-> ({y} : El c)
-> (x : Obj c)
-> ({y} : Obj c)
-> Terminal y
-> Arrow x y ;
-- def terminalAr {c} x {~y} (terminal {~c} y f) = f x ;
{-
fun terminals2iso : ({c} : Category)
-> ({x,y} : El c)
-> ({x,y} : Obj c)
-> (tx : Terminal x)
-> (ty : Terminal y)
-> Iso (terminalAr x ty) (terminalAr y tx) ;
-}
-- def terminals2iso = .. ;
}
}

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

@@ -1,9 +1,9 @@
abstract Morphisms = Categories ** {
cat Iso ({c} : Category) ({x,y} : El c) (Arrow x y) (Arrow y x) ;
cat Iso ({c} : Category) ({x,y} : Obj c) (Arrow x y) (Arrow y x) ;
data iso : ({c} : Category)
-> ({x,y} : El c)
-> ({x,y} : Obj c)
-> (f : Arrow x y)
-> (g : Arrow y x)
-> (EqAr (comp f g) (id y))
@@ -11,7 +11,7 @@ data iso : ({c} : Category)
-> Iso f g ;
fun isoOp : ({c} : Category)
-> ({x,y} : El c)
-> ({x,y} : Obj c)
-> ({f} : Arrow x y)
-> ({g} : Arrow y x)
-> Iso f g
@@ -19,7 +19,7 @@ fun isoOp : ({c} : Category)
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)
-> ({x,y} : Obj c)
-> ({f} : Arrow x y)
-> ({g} : Arrow y x)
-> (Iso f g -> Mono f) ;
@@ -35,7 +35,7 @@ def iso2mono (iso f g id_fg id_gf) =
-- f . h = f . m
fun iso2epi : ({c} : Category)
-> ({x,y} : El c)
-> ({x,y} : Obj c)
-> ({f} : Arrow x y)
-> ({g} : Arrow y x)
-> (Iso f g -> Epi f) ;
@@ -51,20 +51,20 @@ def iso2epi (iso fff g id_fg id_gf) =
(eqCompR eq_hf_mf g))))))))) ; -- (h . f) . g = (m . f) . g
-- h . f = m . f
cat Mono ({c} : Category) ({x,y} : El c) (Arrow x y) ;
cat Mono ({c} : Category) ({x,y} : Obj c) (Arrow x y) ;
data mono : ({c} : Category)
-> ({x,y} : El c)
-> ({x,y} : Obj c)
-> (f : Arrow x y)
-> (({z} : El c) -> (h,m : Arrow z x) -> EqAr (comp f h) (comp f m) -> EqAr h m)
-> (({z} : Obj 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) ;
cat Epi ({c} : Category) ({x,y} : Obj c) (Arrow x y) ;
data epi : ({c} : Category)
-> ({x,y} : El c)
-> ({x,y} : Obj c)
-> (f : Arrow x y)
-> (({z} : El c) -> (h,m : Arrow y z) -> EqAr (comp h f) (comp m f) -> EqAr h m)
-> (({z} : Obj c) -> (h,m : Arrow y z) -> EqAr (comp h f) (comp m f) -> EqAr h m)
-> Epi f ;
}

4
examples/category-theory/NaturalTransform.gf
View File

@@ -4,7 +4,7 @@ cat NT ({c1,c2} : Category) (f,g : Functor c1 c2) ;
data nt : ({c1,c2} : Category)
-> (f,g : Functor c1 c2)
-> ((x : El c1) -> Arrow (mapEl f x) (mapEl g x))
-> ((x : Obj c1) -> Arrow (mapObj f x) (mapObj g x))
-> NT f g ;
}
}