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 $C$ be a category with coproducts (written $+$). A predicate is a map $X\stackrel{p}{\to} X+X$ such that $[id_X,id_X]\circ p=id_X$.
A predicate is hence in particular a coalgebra for the $C$-endofunctor $X\mapsto X+X$.
If we denote the coproduct inclusions by $k_1:X\to X+X$ and $k_2:X\to X+X$, then their coproduct $[k_2,k_1]:X+X\to X+X$ is the swap map (which is a self-inverse equivalence).
For a predicate $p$ the orthocomplement of $p$ is defined to be the composite $p^\perp:=[k_2,k_1]\circ p$. We have $(p^\perp)^\perp\simeq p$.
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 $X\in Set$ is a set and $p:X\to X+X$ is a predicate on $X$, then $p(x)=k_1 x$ or $p(x)=k_2 x$.
In particular we can identify $p$ with a subset $U=\{x|p(x)=k_1 x\}\subseteq X$. Then $\neg U=\{x|p(x)=k_2 x\}=\{x|p^\perp(x)=k_1 x\}$
In $Set$ we have disjoint coproducts such that in our case we have
is a pushout square as well as a pullback square. And in $Set$ we have universal coproducts such that in our case we have $X+X\simeq X$. Now if we assume $[id_X,id_X]\circ p\simeq id_X$ the couniversal property of the coproduct implies that $p$ factors through $k_1$ and $k_2$ 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.