An \(\mathcal {F}\) -coalgebra \((Y,g)\)  is called final is there is a unique
\(\mathcal {F}\) -homomorphism \(\llbracket \_\rrbracket ^F_X\)  from any \(\mathcal {F}\) -coalgebra
\((X,f)\)  to \((Y,g)\) . The final coalgebra represents the universe of all possible
\(\mathcal {F}\) -behaviours and the arrow \(\llbracket \_\rrbracket ^F_X\)  maps every element
(or state) of a coalgebra \(X\)  to its
behaviour [1]}. Two states \(x_1,x_2 \in X\)  are said to be
\(\mathcal {F}\) -behaviourally equivalent, denoted \(\approx _\mathcal {F}\) , iff \(\llbracket x_1\rrbracket ^\mathcal {F}_X = \llbracket x_2\rrbracket ^\mathcal {F}_X\) .
