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. 



Freyd cover of a category.
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.)


