Pushout-complements and basic concepts of grammars in toposes (Q757576)

The author investigates pushouts in toposes by using essentially the theory of binary relations, which he called relational calculus. A characterization of pushouts is given, and also characterizations of the existence of a whole pushout starting from some part of it. For example for a composable pair of morphisms (f,g) any pair of morphisms (h,k) such that (g,k) is the pushout of (f,h) is called a pushout-complement of (f,g). The special case of the topos of directed graphs is closely examined. As an application, an embedding theorem and Church-Rosser theorem on grammars in a topos is proved.