  The theory of types of Church can also be used to build the free topos. For this we take as objects pairs \(A,E\) with \(A\) type and \(E\) a partial equivalence relation, that is a closed term \(E:A \rightarrow A \rightarrow o\) which is symmetric and transitive. We take as morphisms between \(A, E\) and \(B, F\) the relations \(R:A\rightarrow B\rightarrow o\) that are functional that is such that for any \(a:A\) satisfying \(E a a\) there exists one, and only one (modulo \(F)\) element \(b\) of \(B\) such that \(F b b\) and \(R a b\). For the subobject classifier we take the pair \(o, E\) with \(E:o\rightarrow o\rightarrow o\) defined as