\\
              B \ar[r]_{\psi_1} & D \itul{\rm\footnotesize\color{gray}(PB)}
            }$$

Note that the annotation functor from Ex. \[ex:global-annot\] satisfies all properties above, whereas the functors from Ex. \[ex:local-annot\] and \[ex:path-annot\] satisfy both the homomorphism property and the pushout property for standard annotations, but do not satisfy all the remaining requirements [(see Lem. \[lem:global-annot-properties\], \[lem:local-annot-properties\] and \[lem:path-annot-properties\] in App. \[apx:proofs\])]{}.

We will now introduce objects with two annotations, giving lower and upper bounds.

\[def:doubly-annotated-object\] Given a topos $\C$ and a functor $\mathcal{A}\colon \C \to \mathbf{Mon}$, a *doubly annotated object* $A[a_1,a_2]$ is an object $A$ of $\C$ with two annotations $a_1,a_2\in \mathcal{A}(A)$. An arrow $\phi\colon A[a_1,a_2]\to B[b_1,b_2]$, also called a *legal arrow*, is a $\C$-arrow $\phi\colon A\to B$ such that $\mathcal{A}_\phi(a_1)\ge b_1$ and $\mathcal{A}_\phi(a_2) \le b_2$.

The *language of a doubly annotated object* $A[a_1,a_2]$ (also called the language of objects which are abstracted by $A[a_1,a_2]$) is defined as follows: $$\mathcal{L}(A[a_1,a_2]) = \{ X\in \C\mid \mbox{there exists a
      legal arrow $\phi\colon X[s_X,s_X]\to A[a_1,a_2]$}\}$$

Note that legal arrows are closed under composition [@ckn:graph-languages-type-graphs]. Examples of doubly annotated objects are given in Ex. \[ex:annot-rewriting-step\] for global annotations from Ex. \[ex:global-annot\] (providing upper and lower bounds for the number of nodes resp. edges in the preimage of a given 