Freyd cover explained

In the mathematical discipline of category theory, the Freyd cover or scone category is a construction that yields a set-like construction out of a given category. The only requirement is that the original category has a terminal object. The scone category inherits almost any categorical construct the original category has. Scones can be used to generally describe proofs that use logical relations.

The Freyd cover is named after Peter Freyd. The other name, "scone", is intended to suggest that it is like a cone, but with the Sierpiński space in place of the unit interval.

Definition

1 _{Set} \downarrow \operatorname{Hom} _{C(1,-)} .

See also

• Artin gluing

References

• Book: 978-0-444-70368-2 . [{{Google books|fCSJRegkKdoC|keywords=scone|plainurl=yes}} Categories, Allegories ]. Freyd . P. J. . Scedrov . A. . 22 November 1990 . Elsevier Science.
• Book: Lambek . Joachim . Scott . Philip J. . [{{Google books|6PY_emBeGjUC |keywords=Freyd cover|plainurl=yes}} Introduction to higher order categorical logic ]. 1994 . Cambridge Univ. Press . Cambridge . 9780521356534 . Paperback (with corr.), reprinted.
• Book: https://doi.org/10.1007/3-540-56992-8_21 . 10.1007/3-540-56992-8_21 . Notes on sconing and relators . Computer Science Logic . Lecture Notes in Computer Science . 1993 . Mitchell . John C. . Scedrov . Andre . 702 . 352–378 . 978-3-540-56992-3 .
• 10.1305/ndjfl/1093870454 . On the Freyd cover of a topos . 1983 . Moerdijk . Ieke . Notre Dame Journal of Formal Logic . 24 . 4 . 2066/128987 . free .
• Book: Scedrov . Andrej . Scott . Philip J. . A Note on the Friedman Slash and Freyd Covers . Studies in Logic and the Foundations of Mathematics . 1982 . 110 . 443–452. 10.1016/S0049-237X(09)70142-9. 978-0-444-86494-9 .
• Book: 10.1007/BFb0090721 . Constructive Mathematics . Lecture Notes in Mathematics . 1981 . 873 . 978-3-540-10850-4 .

Further reading

• Book: 10.1017/CBO9780511525902.018 . Partial products, bagdomains and hyperlocal toposes §.6, Bagdomains and Scones . Applications of Categories in Computer Science . 1992 . Johnstone . P. T. . 315–339 . 978-0-521-42726-5 .
• 10.1017/S0960129599002741 . Topical categories of domains . 1999 . Vickers . Steven . Mathematical Structures in Computer Science . 9 . 5 . 569–616. Steve Vickers (computer scientist) .
• 10.1145/3474834 . Logical Relations as Types: Proof-Relevant Parametricity for Program Modules . 2021 . Sterling . Jonathan . Harper . Robert . Journal of the ACM . 68 . 6 . 1–47 . 2010.08599 .