Formalizing restriction categories

James Chapman, Tarmo Uustalu, Niccolò Veltri

Research output: Contribution to journalArticle

1 Citation (Scopus)

Abstract

Restriction categories are an abstract axiomatic framework by Cockett and Lack for reasoning about (generalizations of the idea of) partiality of functions. In a restriction category, every map defines an endomap on its domain, the corresponding partial identity map. Restriction categories cover a number of examples of different flavors and are sound and complete with respect to the more synthetic and concrete partial map categories. A partial map category is based on a given category (of total maps) and a map in it is a map from a subobject of the domain. In this paper, we report on an Agda formalization of the first chapters of the theory of restriction categories, including the challenging completeness result. We explain the mathematics formalized, comment on the design decisions we made for the formalization, and illustrate them at work.
LanguageEnglish
Pages1-36
Number of pages36
JournalJournal of Formalized Reasoning
Volume10
Issue number1
DOIs
Publication statusPublished - 10 Mar 2017

Fingerprint

Restriction
Formalization
Partial
Identity mapping
Flavors
Completeness
Reasoning
Acoustic waves
Concretes
Cover

Keywords

  • restriction categories
  • fuctions
  • Agda formalization

Cite this

Chapman, James ; Uustalu, Tarmo ; Veltri, Niccolò. / Formalizing restriction categories. In: Journal of Formalized Reasoning. 2017 ; Vol. 10, No. 1. pp. 1-36.
@article{3de1b2e1ae284e52ad735ca82b98a4ff,
title = "Formalizing restriction categories",
abstract = "Restriction categories are an abstract axiomatic framework by Cockett and Lack for reasoning about (generalizations of the idea of) partiality of functions. In a restriction category, every map defines an endomap on its domain, the corresponding partial identity map. Restriction categories cover a number of examples of different flavors and are sound and complete with respect to the more synthetic and concrete partial map categories. A partial map category is based on a given category (of total maps) and a map in it is a map from a subobject of the domain. In this paper, we report on an Agda formalization of the first chapters of the theory of restriction categories, including the challenging completeness result. We explain the mathematics formalized, comment on the design decisions we made for the formalization, and illustrate them at work.",
keywords = "restriction categories, fuctions, Agda formalization",
author = "James Chapman and Tarmo Uustalu and Niccol{\`o} Veltri",
year = "2017",
month = "3",
day = "10",
doi = "10.6092/issn.1972-5787/6237",
language = "English",
volume = "10",
pages = "1--36",
journal = "Journal of Formalized Reasoning",
issn = "1972-5787",
number = "1",

}

Chapman, J, Uustalu, T & Veltri, N 2017, 'Formalizing restriction categories' Journal of Formalized Reasoning, vol. 10, no. 1, pp. 1-36. https://doi.org/10.6092/issn.1972-5787/6237

Formalizing restriction categories. / Chapman, James; Uustalu, Tarmo; Veltri, Niccolò.

In: Journal of Formalized Reasoning, Vol. 10, No. 1, 10.03.2017, p. 1-36.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Formalizing restriction categories

AU - Chapman, James

AU - Uustalu, Tarmo

AU - Veltri, Niccolò

PY - 2017/3/10

Y1 - 2017/3/10

N2 - Restriction categories are an abstract axiomatic framework by Cockett and Lack for reasoning about (generalizations of the idea of) partiality of functions. In a restriction category, every map defines an endomap on its domain, the corresponding partial identity map. Restriction categories cover a number of examples of different flavors and are sound and complete with respect to the more synthetic and concrete partial map categories. A partial map category is based on a given category (of total maps) and a map in it is a map from a subobject of the domain. In this paper, we report on an Agda formalization of the first chapters of the theory of restriction categories, including the challenging completeness result. We explain the mathematics formalized, comment on the design decisions we made for the formalization, and illustrate them at work.

AB - Restriction categories are an abstract axiomatic framework by Cockett and Lack for reasoning about (generalizations of the idea of) partiality of functions. In a restriction category, every map defines an endomap on its domain, the corresponding partial identity map. Restriction categories cover a number of examples of different flavors and are sound and complete with respect to the more synthetic and concrete partial map categories. A partial map category is based on a given category (of total maps) and a map in it is a map from a subobject of the domain. In this paper, we report on an Agda formalization of the first chapters of the theory of restriction categories, including the challenging completeness result. We explain the mathematics formalized, comment on the design decisions we made for the formalization, and illustrate them at work.

KW - restriction categories

KW - fuctions

KW - Agda formalization

UR - https://jfr.unibo.it/index

U2 - 10.6092/issn.1972-5787/6237

DO - 10.6092/issn.1972-5787/6237

M3 - Article

VL - 10

SP - 1

EP - 36

JO - Journal of Formalized Reasoning

T2 - Journal of Formalized Reasoning

JF - Journal of Formalized Reasoning

SN - 1972-5787

IS - 1

ER -