We consider finite decidable FP-sketches within an arithmetic universe. By an FP-sketch we mean a sketch with terminal and binary product cones. By an arithmetic universe we mean a list-arithmetic pretopos, which is the general categorical definition we give to the concept of arithmetic universe introduced by Andrè Joyal to prove Gödel incompleteness theorems. Then, for finite decidable FP-sketches we prove a constructive version of Ehresmann-Kennison's theorem stating that the category of models of finite decidable FP-sketches in an arithmetic universe is reflective in the corresponding category of graph morphisms. The proof is done by employing the internal dependent type theory of an arithmetic universe.

Reflection into models of finite decidable FP-sketches in an arithmetic universe

MAIETTI, MARIA EMILIA
2005

Abstract

We consider finite decidable FP-sketches within an arithmetic universe. By an FP-sketch we mean a sketch with terminal and binary product cones. By an arithmetic universe we mean a list-arithmetic pretopos, which is the general categorical definition we give to the concept of arithmetic universe introduced by Andrè Joyal to prove Gödel incompleteness theorems. Then, for finite decidable FP-sketches we prove a constructive version of Ehresmann-Kennison's theorem stating that the category of models of finite decidable FP-sketches in an arithmetic universe is reflective in the corresponding category of graph morphisms. The proof is done by employing the internal dependent type theory of an arithmetic universe.
2005
Proceedings of the 10th Conference on Category Theory in Computer Science (CTCS 2004)
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11577/1425280
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? ND
social impact