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

the oposites of two equal arrows are equal arrows

Browse Source
This commit is contained in:
krasimir
2010-02-22 14:38:13 +00:00
parent 59d640088e
commit bcf4bc7d23
1 changed files with 10 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -15,7 +15,7 @@ abstract Categories = {
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} : El c) -> Arrow z y -> Arrow x z -> Arrow x y ;
data eqRefl : ({c} : Category) data eqRefl : ({c} : Category)
-> ({x,y} : El c) -> ({x,y} : El c)
-> (a : Arrow x y) -> (a : Arrow x y)
-> EqAr a a ; -> EqAr a a ;
@@ -77,7 +77,15 @@ abstract Categories = {
-> 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 {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) ; 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) ;
fun eqOp : ({c} : Category)
-> ({x,y} : El c)
-> ({f} : Arrow x y)
-> ({g} : Arrow x y)
-> EqAr f g
-> EqAr (opAr f) (opAr g) ;
def eqOp {c} {x} {y} {f} {f} (eqRefl {c} {x} {y} f) = eqRefl (opAr f) ;
data Slash : (c : Category) data Slash : (c : Category)
-> (x : El c) -> (x : El c)
-> Category ; -> Category ;