HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITION

DOI10.1002/malq.19830291005zbMath0565.03032OpenAlexW2016862652MaRDI QIDQ3679177

R. A. G. Seely

Publication date: 1983

Published in: Mathematical Logic Quarterly (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1002/malq.19830291005

zbMATH Keywords

adjointnessquantifierssubstitutionpull-backfibered categorieshyperdoctrineassociated theorycategory of types

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Fibered categories (18D30)

Related Items (22)

On the semantics of the universal quantifier ⋮ A category-theoretic account of program modules ⋮ Internal diagrams and archetypal reasoning in category theory ⋮ Graded multicategories of polynomial-time realizers ⋮ Dictoses ⋮ Dialectica principles via Gödel doctrines ⋮ On duality and model theory for polyadic spaces ⋮ A general framework for the semantics of type theory ⋮ Polyadic spaces and profinite monoids ⋮ Categorical semantics for higher order polymorphic lambda calculus ⋮ Alpha conversion, conditions on variables and categorical logic ⋮ New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic ⋮ The proof monad ⋮ On the semantics of classical disjunction ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Coherence in linear predicate logic ⋮ A fully abstract semantics for concurrent constraint programming ⋮ A minimalist two-level foundation for constructive mathematics ⋮ On the algebraic structure of declarative programming languages ⋮ Proof-search in type-theoretic languages: An introduction ⋮ Categories with families and first-order logic with dependent sorts

This page was built for publication: HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITION