1: \begin{definition}[Pullback of a morphism from the final object]\strut

2: 

3: Assume $X$ is an effective set.\\

4: By Theorem \ref{th:Final} we can construct $* : El(X) \rightarrow El(1)$

5: defined by $*(u) \eqdef <>$.

6: 

7: Assume $A$ and $\Omega$ are effective sets,

8: $True : El(1) \rightarrow El(\Omega)$ and $f : El(A) \rightarrow El(\Omega)$.\\

9: Then $i$ is the \emph{pullback of} $True$ along $f$ if and only if:

10: \begin{itemize}

11: 

12: \item $B$ is an effective set and $i : El(B) \rightarrow El(A)$.

13: 

14: \item $f \circ i \approx True \circ *$.

15: 

16: \item For all effective set $X$ and for all

17: $\varphi : El(X) \rightarrow El(A)$, if $f \circ \varphi \approx True \circ *$

18: then there exists a unique $\psi : El(X) \rightarrow El(A)$ (modulo $\approx$)

19: such that $i \circ \psi \approx \varphi$.

20: 

21: \end{itemize}

22: $B$ can be seen as the categorical definition of the subset of $A$ which

23: elements satisfies $f$ and with $i$ the injection morphism.

24: \end{definition}

25: