# 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.

-
Could you give a definition of a Freyd Cover? Maybe if you don't know it in the case you're interested in, give the case you do know, and why you think the definition works in your case somehow? – Charles Siegel Jan 17 '10 at 19:43
Ximo: I thought it would be helpful to merge your comment (giving the reference) into the main question, so I did it. You might want to delete that comment now. Also, if you don't like the way I've edited your question, you can edit it yourself (and undo my changes if you want). – Tom Leinster Jan 17 '10 at 21:26

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.)

-

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.

-
So you mean: is it another way to pass from syntactic (what you call crude semantics) to semantic in every case? – Doctor Gibarian Dec 29 '10 at 13:21
It's the other way around: we start with a simple model which may contain elements which do not correspond to any syntactically definable program, and may have unwanted properties. Then, we use a logical relation to construct a cut-down model only containing elements with the desired properties, and then we prove that every program you can define may also be interpreted within this new model. – Neel Krishnaswami Dec 29 '10 at 14:34
"definable program"? Do you mean "definable morphism"? – Uday Reddy Mar 31 '14 at 19:33
I mean there are morphisms which are not the denotation of a term (e.g., parallel-or in the domain theoretic semantics of PCF). – Neel Krishnaswami Mar 31 '14 at 20:35