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

refactor Morphisms.gf and InitialAndTerminal.gf

Browse Source
This commit is contained in:
krasimir
2010-03-15 10:43:20 +00:00
parent 52d5967008
commit 77be515422
2 changed files with 49 additions and 27 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

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

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

@@ -1,6 +1,6 @@
abstract Morphisms = Categories ** {
cat Iso ({c} : Category) (x,y : El c) ;
cat Iso ({c} : Category) ({x,y} : El c) (Arrow x y) (Arrow y x) ;
data iso : ({c} : Category)
-> ({x,y} : El c)
@@ -8,12 +8,23 @@ data iso : ({c} : Category)
-> (g : Arrow y x)
-> (EqAr (comp f g) (id y))
-> (EqAr (comp g f) (id x))
-> Iso x y ;
-> Iso f g ;
fun isoOp : ({c} : Category)
-> ({x,y} : El c)
-> ({f} : Arrow x y)
-> ({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) ;
fun iso2mono : ({c} : Category)
-> ({x,y} : El c)
-> (Iso x y -> Mono x y) ;
def iso2mono {c} {x} {y} (iso {c} {x} {y} f g id_fg id_gf) =
-> ({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) =
mono f (\h,m,eq_fh_fm ->
eqSym (eqTran (eqIdR m) -- h = m
(eqTran (eqCompR id_gf m) -- id . m = h
@@ -26,8 +37,10 @@ def iso2mono {c} {x} {y} (iso {c} {x} {y} f g id_fg id_gf) =
fun iso2epi : ({c} : Category)
-> ({x,y} : El c)
-> (Iso x y -> Epi x y) ;
def iso2epi {c} {x} {y} (iso {c} {x} {y} f g id_fg id_gf) =
-> ({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 ->
eqSym (eqTran (eqIdL m) -- h = m
(eqTran (eqCompL m id_fg) -- m . id = h
@@ -38,21 +51,21 @@ def iso2epi {c} {x} {y} (iso {c} {x} {y} f 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) ;
cat Mono ({c} : Category) ({x,y} : El c) (Arrow x y) ;
data mono : ({c} : Category)
-> ({x,y} : El c)
-> (f : Arrow x y)
-> (({z} : El c) -> (h,m : Arrow z x) -> EqAr (comp f h) (comp f m) -> EqAr h m)
-> Mono x y ;
-> Mono f ;
cat Epi ({c} : Category) (x,y : El c) ;
cat Epi ({c} : Category) ({x,y} : El c) (Arrow x y) ;
data epi : ({c} : Category)
-> ({x,y} : El c)
-> (f : Arrow x y)
-> (({z} : El c) -> (h,m : Arrow y z) -> EqAr (comp h f) (comp m f) -> EqAr h m)
-> Epi x y ;
-> Epi f ;
}