We show that the category whose objects are families of Markov processes on Polish spaces, with a given transition kernel, and whose morphisms are transition probability preserving, surjective continuous maps has semi-pullbacks, i.e., for any pair of morphisms fi:Si→S (i = 1, 2), there exists an object V and morphisms πi:V→Si (i = 1, 2) such that f1∘π1 = f2∘π2. This property holds for various full subcategories, including that of families of Markov processes on locally compact second countable spaces, and in the larger category where the objects are families of Markov processes on analytic spaces and morphisms are transition probability preserving surjective Borel maps. It also follows that the category of probability measures on Polish spaces and measure-preserving continuous surjective maps has semi-pullbacks. A main consequence of our result is that probabilistic bisimulation for labelled Markov processes on all these categories, defined in terms of spans of morphisms, is an equivalence relation.

A special final coalgebra theorem, in the style of Aczel (1988), is proved within standard Zermelo–Fraenkel set theory. Aczel's Anti-Foundation Axiom is replaced by a variant definition of function that admits non-well-founded constructions. Variant ordered pairs and tuples, of possibly infinite length, are special cases of variant functions. Analogues of Aczel's solution and substitution lemmas are proved in the style of Rutten and Turi (1993). The approach is less general than Aczel's, but the treatment of non-well-founded objects is simple and concrete. The final coalgebra of a functor is its greatest fixedpoint.

Compared with previous work (Paulson, 1995a), iterated substitutions and solutions are considered, as well as final coalgebras defined with respect to parameters. The disjoint sum construction is replaced by a smoother treatment of urelements that simplifies many of the derivations.

The theory facilitates machine implementation of recursive definitions by letting both inductive and coinductive definitions be represented as fixed points. It has already been applied to the theorem prover Isabelle (Paulson, 1994).

This paper shows how it is possible to express many techniques of categorical domain theory in the general context of topical categories (where ‘topical’ means internal in the category Top of Grothendieck toposes with geometric morphisms). The underlying topos machinery is hidden by using a geometric form of constructive mathematics, which enables toposes as ‘generalized topological spaces’ to be treated in a transparently spatial way, and also shows the constructivity of the arguments. The theory of strongly algebraic (SFP) domains is given as a case study in which the topical category is Cartesian closed.

This paper is about a categorical approach for modelling the pure (i.e., without constants) call-by-value λ-calculus, defined by Plotkin as a restriction of the call-by-name λ-calculus. In particular, we give the properties that a category Cbv must enjoy to describe a model of call-by-value λ-calculus. The category Cbv is general enough to catch models in Scott Domains and Coherence Spaces.