It is immediate to see that to each \(a \in A\)  there is a unique (up to the equality of \(B\) ) \(b \in B\)  such that
\(u^0(i_A^X(a)) =_Y i_B^Y(b)\) . By Myhill's principle of non-choice (or unique choice), introduced
in [1]}, there is a (necessarily)
unique map \(u^+\)  that makes the above diagram commutative. As this principle is avoided in \(\mathrm {BST}\) , we
prefer to present a morphism \(u\)  in \(\mathrm {\mathbf {Pred}}\)  as a pair \((u^0, u^+)\) .
It is immediate to see that if \(u^0\)  is an embedding, then \(u^+\)  is an embedding, and
if \(u^0\)  is strongly extensional, then \(u^+\)  is also strongly extensional. For a specific set \(X\)  the “fibre” category \(\mathrm {\mathbf {Pred}}_X\)  is the subcategory of \(\mathrm {\mathbf {Pred}}\)  with objects triplets of the form
\((X, A, i_A^X)\)  with \(X\)  fixed, while a morphism \(u \colon (X, A, i_A^X) \rightarrow (X, B, i_B^X)\)  is a pair
\((\mathrm {id}_X, u_{{AB}})\) , and the required commutativity of the following diagram
