Remove contribs and examples

Everything has now been moved to a separate repository at
https://github.com/GrammaticalFramework/gf-contrib
The contents of the examples folder are build during SetupWeb

9 files changed, 0 insertions, 517 deletions

diff --git a/examples/category-theory/Adjoints.gf b/examples/category-theory/Adjoints.gf
deleted file mode 100644
index b4987228d..000000000
--- a/examples/category-theory/Adjoints.gf
+++ /dev/null
@@ -1,16 +0,0 @@
-abstract Adjoints = NaturalTransform ** {

-

-  ----------------------------------------------------------

-  -- Adjoint functors - pair of functors such that

-  -- there is a natural transformation from the identity

-  -- functor to the composition of the functors.

-

-  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 ;

-

-}

diff --git a/examples/category-theory/Categories.gf b/examples/category-theory/Categories.gf
deleted file mode 100644
index b20dccde9..000000000
--- a/examples/category-theory/Categories.gf
+++ /dev/null
@@ -1,201 +0,0 @@
-abstract Categories = {
-
-  -------------------------------------------------------
-  -- Basic category theory: categories, objects, 
-  -- arrows and equality of arrows
-
-  cat Category ;
-      Obj Category ;
-      Arrow ({c} : Category) (Obj c) (Obj c) ;
-      EqAr ({c} : Category) ({x,y} : Obj c) (f,g : Arrow x y) ;
-
-  fun dom : ({c} : Category) -> ({x,y} : Obj c) -> Arrow x y -> Obj c ;
-  def dom   {_} {x} {y} _ = x ;
-
-  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)
-              -> EqAr a b
-              -> EqAr b a ;
-  def  eqSym (eqRefl a) = eqRefl a ;
-
-  fun eqTran :  ({c} : Category)
-             -> ({x,y} : Obj c)
-             -> ({f,g,h} : Arrow x y)
-             -> EqAr f g
-             -> EqAr f h
-             -> EqAr g h ;
-  def eqTran (eqRefl a) eq = eq ;
-
-
-  -------------------------------------------------------
-  -- 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)
-             -> (a : Arrow x y)
-             -> EqAr (comp a (id x)) a ;
-      eqIdR  :  ({c} : Category)
-             -> ({x,y} : Obj c)
-             -> (a : Arrow x y)
-             -> EqAr (comp (id y) a) a ;
-
-  fun eqAssoc :  ({c} : Category)
-              -> ({w,x,y,z} : Obj c)
-              -> (f : Arrow w y)
-              -> (g : Arrow z w)
-              -> (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)
-            -> (x : Obj c)
-            -> Obj (Op c) ;
-       opAr :  ({c} : Category)
-            -> ({x,y} : Obj c)
-            -> (a : Arrow x y)
-            -> Arrow {Op c} (opObj y) (opObj x) ;
-  def  id (opObj x) = opAr (id x) ;
-  def  comp (opAr f) (opAr g) = opAr (comp g f) ;
-
-  fun eqOp :  ({c} : Category)
-           -> ({x,y} : Obj c)
-           -> ({f} : Arrow x y)
-           -> ({g} : Arrow x y)
-           -> EqAr f g
-           -> 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 ;
-       slashObj  :  ({c} : Category)
-                 -> (x,{y} : Obj c)
-                 -> Arrow y x
-                 -> Obj (Slash c x) ;
-       slashAr   :  ({c} : Category)
-                 -> (x,{y,z} : Obj c)
-                 -> ({ay} : Arrow y x)
-                 -> ({az} : Arrow z x)
-                 -> Arrow y z
-                 -> Arrow (slashObj x ay) (slashObj x az) ;
-  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 ;
-       coslashObj:  ({c} : Category)
-                 -> (x,{y} : Obj c)
-                 -> Arrow x y
-                 -> Obj (CoSlash c x) ;
-       coslashAr :  ({c} : Category)
-                 -> (x,{y,z} : Obj c)
-                 -> ({ay} : Arrow x y)
-                 -> ({az} : Arrow x z)
-                 -> Arrow z y
-                 -> Arrow (coslashObj x ay) (coslashObj x az) ;
-  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)
-              -> Obj c1
-              -> Obj c2
-              -> Obj (Prod c1 c2) ;
-       prodAr :  ({c1,c2} : Category)
-              -> ({x1,y1} : Obj c1)
-              -> ({x2,y2} : Obj c2)
-              -> Arrow x1 y1
-              -> Arrow x2 y2
-              -> Arrow (prodObj x1 x2) (prodObj y1 y2) ;
-  def id (prodObj x1 x2) = prodAr (id x1) (id x2) ;
-  def comp (prodAr f1 f2) (prodAr g1 g2) = prodAr (comp f1 g1) (comp f2 g2) ;
-
-  fun fst : ({c1,c2} : Category) -> Obj (Prod c1 c2) -> Obj c1 ;
-  def fst (prodObj x1 _) = x1 ;
-
-  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)
-              -> Obj c1
-              -> Obj (Sum c1 c2) ;
-       sumRObj:  ({c1,c2} : Category)
-              -> Obj c2
-              -> Obj (Sum c1 c2) ;
-       sumLAr :  ({c1,c2} : Category)
-              -> ({x,y} : Obj c1)
-              -> Arrow x y
-              -> Arrow {Sum c1 c2} (sumLObj x) (sumLObj y) ;
-       sumRAr :  ({c1,c2} : Category)
-              -> ({x,y} : Obj c2)
-              -> Arrow x y
-              -> Arrow {Sum c1 c2} (sumRObj x) (sumRObj y) ;
-
-  def  id (sumLObj x) = sumLAr (id x) ;
-       id (sumRObj x) = sumRAr (id x) ;
-
-       comp (sumRAr f) (sumRAr g) = sumRAr (comp f g) ;
-       comp (sumLAr f) (sumLAr g) = sumLAr (comp f g) ;
-
-}
diff --git a/examples/category-theory/CategoryTheory.gf b/examples/category-theory/CategoryTheory.gf
deleted file mode 100644
index 6e3ed3e09..000000000
--- a/examples/category-theory/CategoryTheory.gf
+++ /dev/null
@@ -1,11 +0,0 @@
-abstract CategoryTheory 

-  = Categories

-  , Morphisms

-  , InitialAndTerminal

-  , Functor

-  , NaturalTransform

-  , Equalizer

-  , Adjoints

-  , Monad

-** {

-}
\ No newline at end of file
diff --git a/examples/category-theory/Equalizer.gf b/examples/category-theory/Equalizer.gf
deleted file mode 100644
index 4e12bd199..000000000
--- a/examples/category-theory/Equalizer.gf
+++ /dev/null
@@ -1,49 +0,0 @@
-abstract Equalizer = Morphisms ** {
-
-cat Equalizer ({c} : Category) ({x,y,z} : Obj c) (f,g : Arrow x y) (e : Arrow z x) ;
-
-data equalizer :  ({c} : Category)
-               -> ({x,y,z} : Obj c)
-               -> (f,g : Arrow x y)
-               -> (e : Arrow z x)
-               -> EqAr (comp f e) (comp g e)
-               -> Equalizer f g e ;
-
-fun idEqualizer : ({c} : Category)
-               -> ({x,y} : Obj c)
-               -> (f : Arrow x y)
-               -> Equalizer f f (id x) ;
-def idEqualizer {c} {x} {y} f = equalizer f f (id x) (eqCompL f (eqRefl (id x))) ;
-
-fun equalizer2mono :  ({c} : Category)
-                   -> ({x,y,z} : Obj c)
-                   -> (f,g : Arrow x y)
-                   -> (e : Arrow z x)
-                   -> Equalizer f g e
-                   -> Mono e ;
--- def equalizer2mono = ...
-
-cat CoEqualizer ({c} : Category) ({x,y,z} : Obj c) (e : Arrow y z) (f,g : Arrow x y) ;
-
-data coequalizer :  ({c} : Category)
-                 -> ({x,y,z} : Obj c)
-                 -> (e : Arrow y z)
-                 -> (f,g : Arrow x y)
-                 -> EqAr (comp e f) (comp e g)
-                 -> CoEqualizer e f g ;
-
-fun idCoEqualizer : ({c} : Category)
-                 -> ({x,y} : Obj c)
-                 -> (f : Arrow x y)
-                 -> CoEqualizer (id y) f f ;
-def idCoEqualizer {c} {x} {y} f = coequalizer (id y) f f (eqCompR (eqRefl (id y)) f) ;
-
-fun coequalizer2epi :  ({c} : Category)
-                    -> ({x,y,z} : Obj c)
-                    -> ({e} : Arrow y z)
-                    -> ({f,g} : Arrow x y)
-                    -> CoEqualizer e f g
-                    -> Epi e ;
--- def coequalizer2epi = ...
-
-}
diff --git a/examples/category-theory/Functor.gf b/examples/category-theory/Functor.gf
deleted file mode 100644
index e70254839..000000000
--- a/examples/category-theory/Functor.gf
+++ /dev/null
@@ -1,53 +0,0 @@
-abstract Functor = Categories ** {

-

-  ----------------------------------------------------------

-  -- 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.

-

-  cat Functor (c1, c2 : Category) ;

-

-  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 ;

-

-  -- 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)) ;

-

-  -- 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 -> eqTran (eqSym (mapEqAr f032 f132 (eqid13 x))) (eqid32 (f013 x)))

-                   (\f,g -> eqTran (eqSym (mapEqAr f032 f132 (eqcmp13 f g))) (eqcmp32 (f113 f) (f113 g))) ;

-

-  fun mapObj :  ({c1, c2} : Category)

-            -> Functor c1 c2

-            -> Obj c1

-            -> Obj c2 ;

-  def mapObj (functor f0 f1 _ _) = f0 ;

-

-  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 :  ({c1,c2} : Category)

-              -> ({x,y} : Obj c1)

-              -> ({f,g} : Arrow x y)

-              -> (f0 : Obj c1 -> Obj c2)

-              -> (f1 : Arrow x y -> Arrow (f0 x) (f0 y))

-              -> EqAr f g

-              -> EqAr (f1 f) (f1 g) ;

-  def mapEqAr f0 f1 (eqRefl f) = eqRefl (f1 f) ;

-

-}

diff --git a/examples/category-theory/InitialAndTerminal.gf b/examples/category-theory/InitialAndTerminal.gf
deleted file mode 100644
index b8a9f00c9..000000000
--- a/examples/category-theory/InitialAndTerminal.gf
+++ /dev/null
@@ -1,46 +0,0 @@
-abstract InitialAndTerminal = Morphisms ** {

-

-cat  Initial  ({c} : Category) (Obj c) ;

-data initial  : ({c} : Category)

-              -> (x : Obj c)

-              -> ((y : Obj c) -> Arrow x y)

-              -> Initial x ;

-              

-fun initAr :  ({c} : Category)

-           -> ({x} : Obj c)

-           -> Initial x

-           -> (y : Obj c)

-           -> Arrow x y ;

--- def initAr {~c} {~x} (initial {c} x f) y = f y ;

-{-

-fun initials2iso :  ({c} : Category)

-                 -> ({x,y} : Obj c)

-                 -> (ix : Initial x)

-                 -> (iy : Initial y)

-                 -> Iso (initAr ix y) (initAr iy x) ;

--}

--- def initials2iso = .. ;

-

-

-cat  Terminal ({c} : Category) (Obj c) ;

-data terminal : ({c} : Category)

-              -> (y : Obj c)

-              -> ((x : Obj c) -> Arrow x y)

-              -> Terminal y ;

-

-fun terminalAr :  ({c} : Category)

-               -> (x : Obj c)

-               -> ({y} : Obj c)

-               -> Terminal y

-               -> Arrow x y ;

--- def terminalAr {c} x {~y} (terminal {~c} y f) = f x ;

-{-

-fun terminals2iso :  ({c} : Category)

-                  -> ({x,y} : Obj c)

-                  -> (tx : Terminal x)

-                  -> (ty : Terminal y)

-                  -> Iso (terminalAr x ty) (terminalAr y tx) ;

-                  -}

--- def terminals2iso = .. ;

-

-}

diff --git a/examples/category-theory/Monad.gf b/examples/category-theory/Monad.gf
deleted file mode 100644
index 68612d312..000000000
--- a/examples/category-theory/Monad.gf
+++ /dev/null
@@ -1,30 +0,0 @@
-abstract Monad = Adjoints ** {

-

-cat Monad ({c} : Category) (m : Functor c c) ;

-

-data monad :  ({c} : Category)

-           -> (m : Functor c c)

-           -> NT (compF m m) m

-           -> NT (idF c) m

-           -> Monad m ;

-

-fun adjoints2monad :  ({c,d} : Category)

-                   -> (f : Functor c d)

-                   -> (g : Functor d c)

-                   -> Adjoints f g

-                   -> Monad (compF g f) ;

--- def adjoints2monad = ...

-

-{-

-fun kleisliCat :  ({c} : Category)

-               -> ({m} : Functor c c)

-               -> Monad m

-               -> Category ;

-

-fun monad2adjoints :  ({c} : Category)

-                   -> ({m} : Functor c c)

-                   -> Monad m

-                   -> Adjoints {c} {kleisliCat m} f g

--}

-

-}
\ No newline at end of file
diff --git a/examples/category-theory/Morphisms.gf b/examples/category-theory/Morphisms.gf
deleted file mode 100644
index 002a2656a..000000000
--- a/examples/category-theory/Morphisms.gf
+++ /dev/null
@@ -1,92 +0,0 @@
-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)
-         -> ({x,y} : Obj c)
-         -> (f : Arrow x y)
-         -> (g : Arrow y x)
-         -> (EqAr (comp f g) (id y))
-         -> (EqAr (comp g f) (id x))
-         -> Iso f g ;
-
-fun isoOp : ({c} : Category)
-         -> ({x,y} : Obj c)
-         -> ({f} : Arrow x y)
-         -> ({g} : Arrow y x)
-         -> Iso f g
-         -> 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)
-             -> ({g} : Arrow y x)
-             -> (Iso f g -> Mono f) ;
-def iso2mono (iso 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
-                                            (eqTran (eqAssoc g f m)                                                -- (g . f) . m = h
-                                                    (eqSym (eqTran (eqIdR h)                                       -- g . (f . m) = h
-                                                                   (eqTran (eqCompR id_gf h)                       --      id . h = g . (f . m)
-                                                                           (eqTran (eqAssoc g f h)                 -- (g . f) . h = g . (f . m)
-                                                                                   (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)
-             -> ({g} : Arrow y x)
-             -> (Iso f g -> Epi f) ;
-
-def iso2epi (iso f g id_fg id_gf) =
-        epi f (\h,m,eq_hf_mf -> 
-                      eqSym (eqTran (eqIdL m)                                                                     --           h = m
-                                    (eqTran (eqCompL m id_fg)                                                     --      m . id = h
-                                            (eqTran (eqSym (eqAssoc m f g))                                       -- m . (f . g) = h
-                                                    (eqSym (eqTran (eqIdL h)                                      -- (m . f) . g = h
-                                                                   (eqTran (eqCompL h id_fg)                      --      h . id = (m . f) . g
-                                                                           (eqTran (eqSym (eqAssoc h f g))        -- h . (f . g) = (m . f) . g
-                                                                                   (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)
-          -> ({x,y} : Obj c)
-          -> (f : Arrow x y)
-          -> (({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)
-          -> ({x,y} : Obj c)
-          -> (f : Arrow x y)
-          -> (({z} : Obj c) -> (h,m : Arrow y z) -> EqAr (comp h f) (comp m f) -> EqAr h m)
-          -> Epi f ;
-
-}
diff --git a/examples/category-theory/NaturalTransform.gf b/examples/category-theory/NaturalTransform.gf
deleted file mode 100644
index 60943737c..000000000
--- a/examples/category-theory/NaturalTransform.gf
+++ /dev/null
@@ -1,19 +0,0 @@
-abstract NaturalTransform = Functor ** {
-
-  ----------------------------------------------------------
-  -- Natural transformation - a pair of functors which 
-  -- differ up to an arrow
-
-  cat NT ({c1,c2} : Category) (f,g : Functor c1 c2) ;
-
-  data nt :  ({c1,c2} : Category)
-          -> (f,g : Functor c1 c2)
-          -> (n : (x : Obj c1) -> Arrow (mapObj f x) (mapObj g x))
-          -> (  ({x,y} : Obj c1)
-             -> (ar : Arrow x y)
-             -> EqAr (comp (n y) (mapAr f ar))
-                     (comp (mapAr g ar) (n x))
-             )
-          -> NT f g ;
-
-}