diff options
| -rw-r--r-- | examples/category-theory/Categories.gf | 32 | ||||
| -rw-r--r-- | examples/category-theory/CategoryTheory.gf | 7 | ||||
| -rw-r--r-- | examples/category-theory/InitialAndTerminal.gf | 35 | ||||
| -rw-r--r-- | examples/category-theory/Morphisms.gf | 44 |
4 files changed, 102 insertions, 16 deletions
diff --git a/examples/category-theory/Categories.gf b/examples/category-theory/Categories.gf index 09c474290..71c6795df 100644 --- a/examples/category-theory/Categories.gf +++ b/examples/category-theory/Categories.gf @@ -13,8 +13,8 @@ abstract Categories = { fun id : ({c} : Category) -> (x : El c) -> Arrow x x ; - fun comp : ({c} : Category) -> ({x,y,z} : El c) -> Arrow x y -> Arrow y z -> Arrow x z ; - + fun comp : ({c} : Category) -> ({x,y,z} : El c) -> Arrow z y -> Arrow x z -> Arrow x y ; + eq : ({c} : Category) -> ({x,y} : El c) -> (a : Arrow x y) @@ -27,27 +27,27 @@ abstract Categories = { eqIdL : ({c} : Category) -> ({x,y} : El c) -> (a : Arrow x y) - -> EqAr a (comp a (id y)) ; + -> EqAr a (comp a (id x)) ; eqIdR : ({c} : Category) -> ({x,y} : El c) -> (a : Arrow x y) - -> EqAr a (comp (id x) a) ; + -> EqAr a (comp (id y) a) ; eqComp : ({c} : Category) -> ({w,x,y,z} : El c) - -> (f : Arrow w x) - -> (g : Arrow x y) - -> (h : Arrow y z) + -> (f : Arrow w y) + -> (g : Arrow z w) + -> (h : Arrow x z) -> EqAr (comp f (comp g h)) (comp (comp f g) h) ; - fun Op : (c : Category) - -> Category ; - opEl : ({c} : Category) - -> (x : El c) - -> El (Op c) ; - opAr : ({c} : Category) - -> ({x,y} : El c) - -> (a : Arrow x y) - -> Arrow {Op c} (opEl y) (opEl x) ; + data Op : (c : Category) + -> Category ; + opEl : ({c} : Category) + -> (x : El c) + -> El (Op c) ; + opAr : ({c} : Category) + -> ({x,y} : El c) + -> (a : Arrow x y) + -> Arrow {Op c} (opEl y) (opEl x) ; data Slash : (c : Category) -> (x : El c) diff --git a/examples/category-theory/CategoryTheory.gf b/examples/category-theory/CategoryTheory.gf new file mode 100644 index 000000000..d896ceb35 --- /dev/null +++ b/examples/category-theory/CategoryTheory.gf @@ -0,0 +1,7 @@ +abstract CategoryTheory
+ = Categories
+ , Morphisms
+ , InitialAndTerminal
+
+** {
+}
\ No newline at end of file diff --git a/examples/category-theory/InitialAndTerminal.gf b/examples/category-theory/InitialAndTerminal.gf new file mode 100644 index 000000000..7ac7b0864 --- /dev/null +++ b/examples/category-theory/InitialAndTerminal.gf @@ -0,0 +1,35 @@ +abstract InitialAndTerminal = Morphisms ** {
+
+cat Initial (c : Category) ;
+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 (initial x f) = x ;
+
+fun initials2iso : ({c} : Category)
+ -> ({x,y} : Initial c)
+ -> Iso (initEl x) (initEl y) ;
+-- def initials2iso = .. ;
+
+cat Terminal (c : Category) ;
+data terminal : ({c} : Category)
+ -> (y : El c)
+ -> ((x : El c) -> Arrow x y)
+ -> Terminal c ;
+
+fun termEl : ({c} : Category)
+ -> Terminal c
+ -> El c ;
+def termEl (terminal x f) = x ;
+
+fun terminals2iso : ({c} : Category)
+ -> ({x,y} : Terminal c)
+ -> Iso (termEl x) (termEl y) ;
+-- def terminals2iso = .. ;
+
+}
\ No newline at end of file diff --git a/examples/category-theory/Morphisms.gf b/examples/category-theory/Morphisms.gf new file mode 100644 index 000000000..426419cc0 --- /dev/null +++ b/examples/category-theory/Morphisms.gf @@ -0,0 +1,44 @@ +abstract Morphisms = Categories ** { + +cat Iso ({c} : Category) (x,y : El c) ; + +data iso : ({c} : Category) + -> ({x,y} : El c) + -> (f : Arrow x y) + -> (g : Arrow y x) + -> (EqAr (comp f g) (id y)) + -> (EqAr (comp g f) (id x)) + -> Iso x y ; + +fun iso2mono : ({c} : Category) + -> ({x,y} : El c) + -> (Iso x y -> Mono x y) ; +-- def iso2mono (iso f g eq_fg eq_gf) = (mono f (\h m eq_fh_fm -> ...)) + +-- eqIdR (eqTran eq_gf (eqComp g f h)) : EqAr (comp g (comp f h)) h +-- comp g (comp f m) + +fun iso2epi : ({c} : Category) + -> ({x,y} : El c) + -> (Iso x y -> Epi x y) ; +-- def iso2epi (iso f g eq_fg eq_gf) = (epi f (\h m eq_hf_mf -> ...)) + + +cat Mono ({c} : Category) (x,y : El c) ; + +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 ; + + +cat Epi ({c} : Category) (x,y : El c) ; + +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 ; + +}
\ No newline at end of file |