I’ve couldn’t find any information about the free category built up from that Freyd cover. Where can I find more about the Freyd cover of a category (not a topos!)?
Edit: The definition has been given in Lambek and Scott's "Higher order categorical logic". I think (according to L. Román) it is initial among all categories endowed with products and a weak nno.
Edit: (Added by Tom Leinster) Here's the definition of Freyd cover, taken from Lambek and Scott (22.1). Let $\mathcal{T}$ be a category with terminal object. Its Freyd cover $\hat{\mathcal{T}}$ is the comma category whose objects are the triples $(X, \xi, U)$ where:
- $X$ is a set
- $U$ is an object of $\mathcal{T}$
- $\xi: X \to \mathcal{T}(1, U)$ is a function.
Lambek and Scott emphasize that $\hat{\mathcal{T}}$ has a terminal object and that it comes equipped with a terminal-object-preserving functor $G: \hat{\mathcal{T}} \to \mathcal{T}$. Strictly speaking, the Freyd cover is the pair $(\hat{\mathcal{T}}, G)$, not just the category $\hat{\mathcal{T}}$ itself.