GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-04-13 23:09:31 -06:00
Code Issues Packages Projects Releases Wiki Activity

some more definitions in category theory

Browse Source
This commit is contained in:
krasimir
2010-02-20 16:33:40 +00:00
parent ff30de63ce
commit 8ca24fcad6
2 changed files with 66 additions and 32 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -15,29 +15,56 @@ abstract Categories = {
fun comp : ({c} : Category) -> ({x,y,z} : El c) -> Arrow z y -> Arrow x z -> Arrow x y ;
eq : ({c} : Category)
data eqRefl : ({c} : Category)
-> ({x,y} : El c)
-> (a : Arrow x y)
-> EqAr a a ;
fun eqSym : ({c} : Category)
-> ({x,y} : El c)
-> ({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 ;
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 ;
fun eqCompL : ({c} : Category)
-> ({x,y,z} : El c)
-> ({g,h} : Arrow x z)
-> (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) ;
fun eqCompR : ({c} : Category)
-> ({x,y,z} : El c)
-> ({g,h} : Arrow z y)
-> 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) ;
fun eqIdL : ({c} : Category)
-> ({x,y} : El c)
-> (a : Arrow x y)
-> EqAr a a ;
eqRefl : ({c} : Category)
-> ({x,y} : El c)
-> ({a,b} : Arrow x y)
-> EqAr a b
-> EqAr b a ;
eqIdL : ({c} : Category)
-> EqAr (comp a (id x)) a ;
eqIdR : ({c} : Category)
-> ({x,y} : El c)
-> (a : Arrow x y)
-> EqAr a (comp a (id x)) ;
eqIdR : ({c} : Category)
-> ({x,y} : El c)
-> (a : Arrow x y)
-> EqAr a (comp (id y) a) ;
eqComp : ({c} : Category)
-> ({w,x,y,z} : El c)
-> (f : Arrow w y)
-> (g : Arrow z w)
-> (h : Arrow x z)
-> EqAr (comp f (comp g h)) (comp (comp f g) h) ;
-> EqAr (comp (id y) a) a ;
fun eqAssoc : ({c} : Category)
-> ({w,x,y,z} : El c)
-> (f : Arrow w y)
-> (g : Arrow z w)
-> (h : Arrow x z)
-> EqAr (comp f (comp g h)) (comp (comp f g) h) ;
data Op : (c : Category)
-> Category ;
@@ -48,6 +75,8 @@ 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) ;
data Slash : (c : Category)
-> (x : El c)
@@ -62,8 +91,8 @@ abstract Categories = {
-> ({az} : Arrow z x)
-> Arrow y z
-> Arrow (slashEl x ay) (slashEl x az) ;
def id (slashEl x {y} a) = slashAr x (id y) ;
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) ;
data CoSlash : (c : Category)
-> (x : El c)
@@ -75,10 +104,11 @@ abstract Categories = {
coslashAr : ({c} : Category)
-> (x,{y,z} : El c)
-> ({ay} : Arrow x y)
-> ({az} : 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) ;
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) ;
data Prod : (c1,c2 : Category)
-> Category ;
@@ -92,13 +122,14 @@ abstract Categories = {
-> Arrow x1 y1
-> Arrow x2 y2
-> Arrow (prodEl x1 x2) (prodEl y1 y2) ;
def id (prodEl x1 x2) = prodAr (id x1) (id x2) ;
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) ;
fun fst : ({c1,c2} : Category) -> El (Prod c1 c2) -> El c1 ;
def fst (prodEl x1 _) = x1 ;
def fst {c1} {c2} (prodEl {c1} {c2} x1 _) = x1 ;
fun snd : ({c1,c2} : Category) -> El (Prod c1 c2) -> El c2 ;
def snd (prodEl _ x2) = x2 ;
def snd {c1} {c2} (prodEl {c1} {c2} _ x2) = x2 ;
data Sum : (c1,c2 : Category)
-> Category ;
@@ -111,12 +142,15 @@ abstract Categories = {
sumLAr : ({c1,c2} : Category)
-> ({x,y} : El c1)
-> Arrow x y
-> Arrow (sumLEl x) (sumLEl y) ;
-> Arrow {Sum c1 c2} (sumLEl x) (sumLEl y) ;
sumRAr : ({c1,c2} : Category)
-> ({x,y} : El c2)
-> Arrow x y
-> Arrow (sumREl x) (sumREl y) ;
def id (sumLEl x) = sumLAr (id x) ;
id (sumREl x) = sumRAr (id x) ;
-> 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) ;
}

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

@@ -9,7 +9,7 @@ data initial : ({c} : Category)
fun initEl : ({c} : Category)
-> Initial c
-> El c ;
def initEl (initial x f) = x ;
def initEl {c} (initial {c} x f) = x ;
fun initials2iso : ({c} : Category)
-> ({x,y} : Initial c)
@@ -25,7 +25,7 @@ data terminal : ({c} : Category)
fun termEl : ({c} : Category)
-> Terminal c
-> El c ;
def termEl (terminal x f) = x ;
def termEl {c} (terminal {c} x f) = x ;
fun terminals2iso : ({c} : Category)
-> ({x,y} : Terminal c)