diff --git a/Automata.hs b/Automata.hs
new file mode 100644
index 0000000..35dacd3
--- /dev/null
+++ b/Automata.hs
@@ -0,0 +1,56 @@
+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, TypeOperators, ScopedTypeVariables, OverlappingInstances #-}
+
+import Control.Monad.Instances
+import Control.Compose
+import Coalgebra
+
+-- F X = 2 x X^A, for some fixed alphabet A
+type F a = (,) Bool `O` ((->) a)
+
+-- Fixpoint, ie languages
+type Language a = Mu (F a)
+
+-- basic constructor
+ctor :: Bool -> (a -> Language a) -> Language a
+ctor b t = phi (O (b, t))
+
+-- For every (F a)-coalgebra x, there is a arrow x -> Language a
+-- and it is unique, so `Language a` is the final (F a)-coalgebra!
+sem :: (Coalgebra (F a) x) => x -> Language a
+sem s = ctor b (\w -> sem $ trans w) where O (b, trans) = psi s
+
+-- auciliry function
+is_member :: [a] -> Language a -> Bool
+is_member [] l = b where O (b, _) = psi l
+is_member (a:r) l = is_member r (trans a) where O (_, trans) = psi l
+
+
+
+-- Our alphabet
+data A = A | B
+	deriving Show
+
+-- Our example automaton, we will look at its language given by sem
+data X = One | Two | Three
+trans :: X -> A -> X
+trans One A = Two
+trans One B = Three
+trans Two A = Three
+trans Two B = One
+trans Three _ = Three
+
+fin :: X -> Bool
+fin One = True;
+fin Two = True;
+fin _ = False;
+
+instance Coalgebra (F A) X where
+	psi x = O (fin x, trans x)
+
+
+-- Test a word against it
+show_member word = putStrLn $ show (word, is_member word (sem One :: Language A))
+
+main = do
+	let words = [[A], [A,B], [A,B,B], [A,B,B,A], [A,B,A,B,A]]
+	sequence $ map show_member words
\ No newline at end of file
diff --git a/Coalgebra.hs b/Coalgebra.hs
index 244b776..9459d78 100644
--- a/Coalgebra.hs
+++ b/Coalgebra.hs
@@ -1,13 +1,13 @@
-{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FunctionalDependencies #-}
 module Coalgebra where
 
-import Control.Monad
+import Control.Monad.Instances
 
--- Definitions for (co)algebras
-class Functor f => Algebra f m where
+-- Definitions for (co)algebras, adding fundeps helped in the Automata case...
+class Functor f => Algebra f m | m -> f where
     phi :: f m -> m
  
-class Functor f => Coalgebra f m where
+class Functor f => Coalgebra f m | m -> f where
     psi :: m -> f m
 
 -- Fixpoint, ie f (Mu f) = Mu f
diff --git a/Streams.hs b/Streams.hs
index 5350153..6833144 100644
--- a/Streams.hs
+++ b/Streams.hs
@@ -3,16 +3,17 @@
 import Control.Monad.Instances
 import Coalgebra
 
--- F X = A x X, for a fixed A, The prelude already provides the functor instance :)
+-- F X = A x X, for a fixed A, this has a functor instance
 type F a = (,) a
 
--- This will give the fixpoint, ie a coalgebra.
+-- This will give the fixpoint, ie a coalgebra, because F is a functor
 type Stream a = Mu (F a)
 
+-- basic constructor
 (+:+) :: a -> Stream a -> Stream a
-(+:+) a s = In (a, s)
+(+:+) a s = phi (a, s)
 
--- For every other (F a)-coalgebra x, there is a arrow x -> Stream a
+-- For every (F a)-coalgebra x, there is a arrow x -> Stream a
 -- and it is unique, so `Stream a` is the final (F a)-coalgebra!
 sem :: (Coalgebra (F a) x) => x -> Stream a
 sem x = x0 +:+ sem x' where (x0, x') = psi x
@@ -22,7 +23,7 @@ toList :: Stream a -> [a]
 toList s = a0 : toList a' where (a0, a') = psi s
 
 
--- example, with a very simple (F Int)-coalgebra, 1 -> 2, 2 -> 3, 3 -> 2
+-- example with a very simple (F Int)-coalgebra, 1 -> 2, 2 -> 3, 3 -> 2
 data X = One | Two | Three
 instance Coalgebra (F Int) X where
 	psi One = (1, Two)