 The final coalgebra of a functor may be regarded as a space of complete observations. (As with all our points in this section, this statement is mainly for functors on Set, and the notion of “complete observation” is, of course, merely suggestive.) For example, let  AtProp be a set whose elements are called atomic propositions, and consider the functor F(a) = ℘fin(a) × ℘(AtProp ).  A coalgebra for this is a set a together with one map of a into its finite subsets, and another map into the collection of sets of atomic propositions. Putting the two maps together gives a finitely-branching Kripke model: each point has finitely many children and some set of atomic propositions.  Now modal logic gives us a way of “observing” properties of points in coalgebras (Kripke models).  And the record of everything that one could observe from a point is the modal theory of that point.  Further, one may take the collection of all theories of all points in all finitely-branching Kripke models and make this collection (it is a set) into the carrier of a final coalgebra for the functor.  Indeed, this would be one way to construct a final coalgebra. 