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

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 f3c6acc6dc
commit 34a8b768eb
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 ;
data eqRefl : ({c} : Category)
data eqRefl : ({c} : Category)
-> ({x,y} : El c)
-> (a : Arrow x y)
-> EqAr a a ;
@@ -77,7 +77,15 @@ abstract Categories = {
-> 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) ;
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)
-> (x : El c)
-> Category ;