2026-07-30T14:29:15Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:27032 2026-07-30T09:16:25Z ddc:004 open_access

Functional Representability in Local Set Theories Ruiz Hernández, Enrique Solórzano, Pedro local set theories function symbols categorical logic In general local set theories (LST), there is an incomplete representability as (x↦τ) for syntactic functions, i.e. those given by descriptions of the form ∀ x∃!yγ, for some formula γ. The well-known equivalence theorem establishes among other things that it is possible to produce a well-termed local set theory that extends any given LST. However, the natural translation between the corresponding languages still does not guarantee strict functional representability, but only up to isomorphisms. In this report, natural isomorphisms that are compatible with reasoning internally in the original LST are made explicit and explored in more generality. The internal translation along them is exhibited to be compatible with all logical operations; syntactic functions naturally represent themselves in a robust way as described in the main results. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Enrique Ruiz Hernández and Pedro Solórzano 2026 Is Part Of LIPIcs, Volume 384, 31st International Conference on Types for Proofs and Programs (TYPES 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2025.14 urn:nbn:de:0030-drops-270323 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.14 eng https://creativecommons.org/licenses/by/4.0/legalcode