In (Jacobs 12) the approach to categorical logic where the substrate carrying the logical notions are Heyting algebras of subobjects in a topos is replaced by a new one where the substrate is effect algebra of predicates in extensive categories.
Let be a category with coproducts (written ). A predicate is a map such that .
A predicate is hence in particular a coalgebra for the -endofunctor .
If we denote the coproduct inclusions by and , then their coproduct is the swap map (which is a self-inverse equivalence).
For a predicate the orthocomplement of is defined to be the composite . We have .
In a extensive category we have the following diagrams involving coproducts and pullbacks:
(…lots of diagrams…)
Predicates with the operations defined by (…) assemble to an effect algebra called the effect algebra of predicates.
If is a set and is a predicate on , then or .
In particular we can identify with a subset . Then
In we have disjoint coproducts such that in our case we have
is a pushout square as well as a pullback square. And in we have universal coproducts such that in our case we have . Now if we assume the couniversal property of the coproduct implies that factors through and followed by an equivalence.
A category having disjoint- and universal coproducts is called an extensive category.
Further examples are listed at
some of the examples at coalgebra for an endofunctor
Created on January 8, 2013 at 03:47:33. See the history of this page for a list of all contributions to it.