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

some comments in the code for category theory

Browse Source
This commit is contained in:
krasimir
2010-06-01 06:56:34 +00:00
parent 5e0d04d0f5
commit d73ed8ba2e
5 changed files with 132 additions and 56 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -1,11 +1,16 @@
abstract Adjoints = NaturalTransform ** {
cat Adjoints ({c1,c2} : Category) (Functor c1 c2) (Functor c2 c1) ;
----------------------------------------------------------
-- Adjoint functors - pair of functors such that
-- there is a natural transformation from the identity
-- functor to the composition of the functors.
data adjoints : ({c1,c2} : Category)
-> (f : Functor c1 c2)
-> (g : Functor c2 c1)
-> NT (idF c1) (compF g f)
-> Adjoints f g ;
cat Adjoints ({c1,c2} : Category) (Functor c1 c2) (Functor c2 c1) ;
}
data adjoints : ({c1,c2} : Category)
-> (f : Functor c1 c2)
-> (g : Functor c2 c1)
-> NT (idF c1) (compF g f)
-> Adjoints f g ;
}

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

@@ -1,5 +1,9 @@
abstract Categories = {
-------------------------------------------------------
-- Basic category theory: categories, objects,
-- arrows and equality of arrows
cat Category ;
Obj Category ;
Arrow ({c} : Category) (Obj c) (Obj c) ;
@@ -11,14 +15,23 @@ abstract Categories = {
fun codom : ({c} : Category) -> ({x,y} : Obj c) -> Arrow x y -> Obj c ;
def codom {_} {x} {y} _ = y ;
-- 'id x' is the identity arrow for object x
fun id : ({c} : Category) -> (x : Obj c) -> Arrow x x ;
-- composition of arrows
fun comp : ({c} : Category) -> ({x,y,z} : Obj c) -> Arrow z y -> Arrow x z -> Arrow x y ;
-------------------------------------------------------
-- The basic equality properties: reflexive,
-- symetric and transitive relation.
-- Only the reflexivity is an axiom.
data eqRefl : ({c} : Category)
-> ({x,y} : Obj c)
-> (a : Arrow x y)
-> EqAr a a ;
fun eqSym : ({c} : Category)
-> ({x,y} : Obj c)
-> ({a,b} : Arrow x y)
@@ -34,21 +47,18 @@ abstract Categories = {
-> EqAr g h ;
def eqTran (eqRefl a) eq = eq ;
fun eqCompL : ({c} : Category)
-> ({x,y,z} : Obj c)
-> ({g,h} : Arrow x z)
-> (f : Arrow z y)
-> EqAr g h
-> EqAr (comp f g) (comp f h) ;
def eqCompL f (eqRefl g) = eqRefl (comp f g) ;
fun eqCompR : ({c} : Category)
-> ({x,y,z} : Obj c)
-> ({g,h} : Arrow z y)
-> EqAr g h
-> (f : Arrow x z)
-> EqAr (comp g f) (comp h f) ;
def eqCompR (eqRefl g) f = eqRefl (comp g f) ;
-------------------------------------------------------
-- Now we prove some theorems which are specific for
-- the equality of arrows
--
-- First we assert the axioms:
--
-- a . id == id . a == a
-- f . (g . h) == (f . g) . h
--
-- and after that we prove that the composition
-- preserves the equality.
fun eqIdL : ({c} : Category)
-> ({x,y} : Obj c)
@@ -66,6 +76,28 @@ abstract Categories = {
-> (h : Arrow x z)
-> EqAr (comp f (comp g h)) (comp (comp f g) h) ;
fun eqCompL : ({c} : Category)
-> ({x,y,z} : Obj c)
-> ({g,h} : Arrow x z)
-> (f : Arrow z y)
-> EqAr g h
-> EqAr (comp f g) (comp f h) ;
def eqCompL f (eqRefl g) = eqRefl (comp f g) ;
fun eqCompR : ({c} : Category)
-> ({x,y,z} : Obj c)
-> ({g,h} : Arrow z y)
-> EqAr g h
-> (f : Arrow x z)
-> EqAr (comp g f) (comp h f) ;
def eqCompR (eqRefl g) f = eqRefl (comp g f) ;
-------------------------------------------------------
-- Operations over categories
--
-- 1. Dual category
data Op : (c : Category)
-> Category ;
opObj: ({c} : Category)
@@ -86,6 +118,7 @@ abstract Categories = {
-> EqAr (opAr f) (opAr g) ;
def eqOp (eqRefl f) = eqRefl (opAr f) ;
-- 2. Slash of a category
data Slash : (c : Category)
-> (x : Obj c)
-> Category ;
@@ -102,6 +135,7 @@ abstract Categories = {
def id (slashObj x {y} a) = slashAr x (id y) ;
def comp (slashAr t azy) (slashAr ~t axz) = slashAr t (comp azy axz) ;
-- 3. CoSlash of a category
data CoSlash : (c : Category)
-> (x : Obj c)
-> Category ;
@@ -118,6 +152,7 @@ abstract Categories = {
def id (coslashObj x {y} a) = coslashAr x (id y) ;
def comp (coslashAr t ayz) (coslashAr ~t azx) = coslashAr t (comp azx ayz) ;
-- 4. Cartesian product of two categories
data Prod : (c1,c2 : Category)
-> Category ;
prodObj: ({c1,c2} : Category)
@@ -139,6 +174,7 @@ abstract Categories = {
fun snd : ({c1,c2} : Category) -> Obj (Prod c1 c2) -> Obj c2 ;
def snd (prodObj _ x2) = x2 ;
-- 5. Sum of two categories
data Sum : (c1,c2 : Category)
-> Category ;
sumLObj: ({c1,c2} : Category)

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

@@ -1,40 +1,49 @@
abstract Functor = Categories ** {
cat Functor (c1, c2 : Category) ;
----------------------------------------------------------
-- Functor - an arrow (a morphism) between two categories
--
-- The functor is defined by two morphisms - one for the
-- objects and one for the arrows. We also require that
-- the morphisms preserve the categorial structure.
data functor : ({c1, c2} : Category)
-> (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 ;
cat Functor (c1, c2 : Category) ;
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)) ;
data functor : ({c1, c2} : Category)
-> (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 compF : ({c1,c2,c3} : Category) -> Functor c3 c2 -> Functor c1 c3 -> Functor c1 c2 ;
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) ? ;
-- identity functor
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)) ;
fun mapObj : ({c1, c2} : Category)
-> Functor c1 c2
-> Obj c1
-> Obj c2 ;
def mapObj (functor f0 f1 _ _) = f0 ;
-- composition of two functors
fun compF : ({c1,c2,c3} : Category) -> Functor c3 c2 -> Functor c1 c3 -> Functor c1 c2 ;
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 mapAr : ({c1, c2} : Category)
-> ({x,y} : Obj c1)
-> (f : Functor c1 c2)
-> Arrow x y
-> Arrow (mapObj f x) (mapObj f y) ;
def mapAr (functor f0 f1 _ _) = f1 ;
fun mapObj : ({c1, c2} : Category)
-> Functor c1 c2
-> Obj c1
-> Obj c2 ;
def mapObj (functor f0 f1 _ _) = f0 ;
fun mapEqAr : ({c} : Category)
-> ({x,y} : Obj c)
-> ({f,g} : Arrow x y)
-> (func : Arrow x y -> Arrow x y)
-> EqAr f g
-> EqAr (func f) (func g) ;
def mapEqAr func (eqRefl f) = eqRefl (func f) ;
fun mapAr : ({c1, c2} : Category)
-> ({x,y} : Obj c1)
-> (f : Functor c1 c2)
-> Arrow x y
-> Arrow (mapObj f x) (mapObj f y) ;
def mapAr (functor f0 f1 _ _) = f1 ;
fun mapEqAr : ({c} : Category)
-> ({x,y} : Obj c)
-> ({f,g} : Arrow x y)
-> (func : Arrow x y -> Arrow x y)
-> EqAr f g
-> EqAr (func f) (func g) ;
def mapEqAr func (eqRefl f) = eqRefl (func f) ;
}

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

@@ -1,5 +1,9 @@
abstract Morphisms = Categories ** {
-------------------------------------------------------
-- 1. Isomorphism - pair of arrows whose composition
-- is the identity arrow
cat Iso ({c} : Category) ({x,y} : Obj c) (Arrow x y) (Arrow y x) ;
data iso : ({c} : Category)
@@ -18,6 +22,7 @@ fun isoOp : ({c} : Category)
-> Iso (opAr g) (opAr f) ;
def isoOp (iso f g id_fg id_gf) = iso (opAr g) (opAr f) (eqOp id_fg) (eqOp id_gf) ;
-- every isomorphism is also monomorphism
fun iso2mono : ({c} : Category)
-> ({x,y} : Obj c)
-> ({f} : Arrow x y)
@@ -34,6 +39,7 @@ def iso2mono (iso f g id_fg id_gf) =
(eqCompL g eq_fh_fm))))))))) ; -- g . (f . h) = g . (f . m)
-- f . h = f . m
-- every isomorphism is also epimorphism
fun iso2epi : ({c} : Category)
-> ({x,y} : Obj c)
-> ({f} : Arrow x y)
@@ -51,6 +57,14 @@ def iso2epi (iso fff g id_fg id_gf) =
(eqCompR eq_hf_mf g))))))))) ; -- (h . f) . g = (m . f) . g
-- h . f = m . f
-------------------------------------------------------
-- 2. Monomorphism - an arrow f such that:
--
-- f . h == f . m ==> h == m
--
-- for every h and m.
cat Mono ({c} : Category) ({x,y} : Obj c) (Arrow x y) ;
data mono : ({c} : Category)
@@ -59,6 +73,14 @@ data mono : ({c} : Category)
-> (({z} : Obj c) -> (h,m : Arrow z x) -> EqAr (comp f h) (comp f m) -> EqAr h m)
-> Mono f ;
-------------------------------------------------------
-- 3. Epimorphism - an arrow f such that:
--
-- h . f == m . f ==> h == m
--
-- for every h and m.
cat Epi ({c} : Category) ({x,y} : Obj c) (Arrow x y) ;
data epi : ({c} : Category)

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

@@ -1,10 +1,14 @@
abstract NaturalTransform = Functor ** {
cat NT ({c1,c2} : Category) (f,g : Functor c1 c2) ;
----------------------------------------------------------
-- Natural transformation - a pair of functors which
-- differ up to an arrow
data nt : ({c1,c2} : Category)
-> (f,g : Functor c1 c2)
-> ((x : Obj c1) -> Arrow (mapObj f x) (mapObj g x))
-> NT f g ;
cat NT ({c1,c2} : Category) (f,g : Functor c1 c2) ;
data nt : ({c1,c2} : Category)
-> (f,g : Functor c1 c2)
-> ((x : Obj c1) -> Arrow (mapObj f x) (mapObj g x))
-> NT f g ;
}