Freyd cover of a category. 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. 
 A: I don't know anything about it myself, but here are some other phrases you might try looking up.  
The Freyd cover of a category is sometimes known as the Sierpinski cone, or "scone".  It's also a special case of Artin gluing.  Given a category $\mathcal{T}$ and a functor $F: \mathcal{T} \to \mathbf{Set}$, the Artin gluing of $F$ is the comma category $\mathbf{Set}\downarrow F$ whose objects are triples $(X, \xi, U)$ where:


*

*$X$ is a set

*$T$ is an object of $\mathcal{T}$

*$\xi$ is a function $X \to F(U)$.


So the Freyd cover is the special case $F = \mathcal{T}(1, -)$. 
You can find more on Artin gluing in this important (and nice) paper:

Aurelio Carboni, Peter Johnstone, Connected limits, familial representability and Artin glueing, Mathematical Structures in Computer Science 5 (1995), 441--459

plus 

Aurelio Carboni, Peter Johnstone, Corrigenda to 'Connected limits...', Mathematical Structures in Computer Science 14 (2004), 185--187.

(Incidentally, my Oxford English Dictionary tells me that the correct spelling is 'gluing', but some people, such as these authors, use 'glueing'.  I'm sure Peter Johnstone has a reason.)
A: Freyd covers are a fundamental tool in the semantics of programming languages. Here, the technique is called "logical relations" or sometimes "Tait-Girard reducibility candidates". 
The general idea is that you start with a crude categorical semantics of a programming language, which does not validate all the properties you want, and then use a Freyd cover to show that every definable program actually does satisfy those properties. We  use these things when the category in question is closed (monoidal or cartesian), but it does not necessarily have to form a topos. 
John Mitchell and Andre Scedrov have a paper, "Notes on Sconing and Relators", in which they study the applications to programming languages. 
