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.
Scedrov, Andrej; Scott, Philip J. (1982). "A Note on the Friedman Slash and Freyd Covers". Studies in Logic and the Foundations of Mathematics. Vol. 110. pp. 443–452. doi:10.1016/S0049-237X(09)70142-9. ISBN978-0-444-86494-9.
Johnstone, P. T. (1992). "Partial products, bagdomains and hyperlocal toposes §.6, Bagdomains and Scones". Applications of Categories in Computer Science. pp. 315–339. doi:10.1017/CBO9780511525902.018. ISBN978-0-521-42726-5.
Sterling, Jonathan; Harper, Robert (2021). "Logical Relations as Types: Proof-Relevant Parametricity for Program Modules". Journal of the ACM. 68 (6): 1–47. arXiv:2010.08599. doi:10.1145/3474834.