1: \begin{definition}

2: \label{def:totpredcat}

3: Let $\cat{B}$ be an effectus in total form. We write

4: $\Pred(\cat{B})$\index{N}{cat@$\Pred(\cat{B})$ category of predicates

5:   in an effectus in total form $\cat{B}$} for the category with:

6: \begin{itemize}

7: \item objects are pairs $(X,p)$ where $p\in\Pred(X)$ is a predicate

8:   $p\colon X \rightarrow 1+1$ on $X$; often we simply talk about

9:   objects $p$ in $\Pred(\cat{B})$ when the carrier $X$ is clear from

10:   the context;

11: 

12: \item morphisms $f\colon (X,p) \rightarrow (Y,q)$ in $\Pred(\cat{B})$

13:   are maps $f\colon X \rightarrow Y$ in $\cat{B}$ with an inequality:

14: $$\begin{array}{rcl}

15: p

16: & \leq &

17: \tbox{f}(q).

18: \end{array}$$

19: 

20: \noindent We recall that $\tbox{f}(q) = q \after f$ is total

21: substitution, which is a map of effect modules by

22: Theorem~\ref{thm:effectusEMod}.

23: \end{itemize}

24: 

25: \noindent We obtain a category $\Pred(\cat{B})$ by

26: Exercise~\ref{exc:subst}~\eqref{exc:subst:totalfun}. It comes equipped

27: with a forgetful functor $\Pred(\cat{B}) \rightarrow \cat{B}$ which is

28: so trivial that we don't bother to give it a name.

29: 

30: There are truth and falsity functors $\one, \zero \colon \cat{B}

31: \rightarrow \Pred(\cat{B})$\index{N}{$\zero$,!falsity

32:   functor}\index{N}{$\one$,!truth functor} given by the truth/top

33: element $\one(X)\in\Pred(X)$ and the falsity/bottom $\zero(X)

34: \in\Pred(X)$ respectively. These functors form left and right adjoints

35: to the forgetful functor in:

36: \begin{equation}

37: \label{diag:totpredzeroone}

38: \vcenter{\xymatrix@R-.5pc{

39: \Pred(\cat{B})\ar[d]_{\dashv\;}^{\;\dashv}

40: \\

41: \cat{B}\ar@/^4ex/[u]^(0.4){\zero\!}\ar@/_4ex/[u]_(0.4){\!\one}

42: }}

43: \end{equation}

44: \end{definition}

45: