The scope of final semantics is quite large. We can also represent observational equivalencies which are not congruencies as was not the case in the initial semantics approach, and if we use non well founded sets, we can even go beyond w-continuos semantics, and be able to distinguish between these two different kinds id metamodels. There is very natural way of explaining categorically co-induction and induction in terms of algebras and co-algebras. And final semantics seems to be precisely the right level of abstraction for describing these two very important features. So, we have two metamodels which essentially try to address the same kind of general concepts, but with somewhat different tools. In logical framework we had higher order constructive type theory, here we have a special class of categorical semantics.

---