The existential completion

MaRDI QIDQ5129224zbMATH OpenFDO

Authors Davide Trotta

Publication date 26 October 2020

Full work available at URL https://arxiv.org/abs/2108.03416, http://www.tac.mta.ca/tac/volumes/35/43/35-43abs.html

IPFS File on IPFS (Hint: this is only the Hash - if you get a timeout, this file is not available on our server.)

zbMATH Keywords

doctrinesexistential completionproperty-like monadtripos

Mathematics Subject Classification ID

Theories (e.g., algebraic theories), structure, and semantics (18C10) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15)

Abstract: We determine the existential completion of a primary doctrine, and we prove that the 2-monad obtained from it is lax-idempotent, and that the 2-category of existential doctrines is isomorphic to the 2-category of algebras for this 2-monad. We also show that the existential completion of an elementary doctrine is again elementary. Finally we extend the notion of exact completion of an elementary existential doctrine to an arbitrary elementary doctrine.

Recommendations

• A characterization of generalized existential completions
• Elementary doctrines as coalgebras
• Unifying exact completions
• Elementary quotient completion
• Relating quotient completions via categorical logic

Cites work

• A 2-categories companion
• A Unified Category-theoretic Semantics for Binding Signatures in Substructural Logics
• Adjointness in Foundations
• Coherence for pseudodistributive laws revisited
• Elementary quotient completion
• Factorization systems and fibrations: toward a fibred Birkhoff variety theorem
• scientific article; zbMATH DE number 19493 (Why is no real title available?)
• scientific article; zbMATH DE number 3522194 (Why is no real title available?)
• scientific article; zbMATH DE number 1271223 (Why is no real title available?)
• scientific article; zbMATH DE number 626734 (Why is no real title available?)
• scientific article; zbMATH DE number 1129148 (Why is no real title available?)
• scientific article; zbMATH DE number 3794304 (Why is no real title available?)
• scientific article; zbMATH DE number 3370546 (Why is no real title available?)
• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• Pseudo-distributive laws and axiomatics for variable binding
• Quotient completion for the foundation of constructive mathematics
• Regular and exact completions
• Relating categorical semantics for intuitionistic linear logic
• Some free constructions in realizability and proof theory
• Tripos theory
• Tripos theory in retrospect
• Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator
• Two-dimensional monad theory
• Unifying exact completions

Cited in

(16)

• Dialectica logical principles
• Elementary doctrines as coalgebras
• Unifying exact completions
• Dialectica principles via Gödel doctrines
• A characterization of generalized existential completions
• Categories of partial equivalence relations as localizations
• Tightly bounded completions
• Elementary quotient completion
• Relating quotient completions via categorical logic
• A presheaf semantics for quantified temporal logics
• Quotients, pure existential completions and arithmetic universes
• Uniform preorders and partial combinatory algebras
• Quantifier-free formulas and quantifier alternation depth in doctrines
• Biased elementary doctrines and quotient completions
• Categorifying computable reducibilities
• A topos for extended Weihrauch degrees

This page was built for publication: The existential completion

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5129224)