The universal exponentiable arrow

DOI10.1016/J.JPAA.2021.106991OpenAlexW4206352891MaRDI QIDQ2078410

Taichi Uemura

Publication date: 28 February 2022

Published in: Journal of Pure and Applied Algebra (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2001.09940

zbMATH Keywords

exponentiable arrowgeneralized algebraic theory

Mathematics Subject Classification ID

Adjoint functors (universal constructions, reflective subcategories, Kan extensions, etc.) (18A40) Theories (e.g., algebraic theories), structure, and semantics (18C10)

Related Items (1)

A general framework for the semantics of type theory

Uses Software

• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Exponentiable morphisms, partial products and pullback complements
• Cartesianness: topological spaces, uniform spaces, and affine schemes
• Wellfounded trees in categories
• Combinatorial structure of type dependency
• Lokal präsentierbare Kategorien. (Locally presentable categories)
• Containers: Constructing strictly positive types
• Natural models of homotopy type theory
• Discrete Generalised Polynomial Functors
• Monads Need Not Be Endofunctors
• Second-Order Algebraic Theories
• A framework for defining logics
• Polynomial functors and polynomial monads
• Local fibred right adjoints are polynomial
• Polynomials in categories with pullbacks
• Types for Proofs and Programs
• FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES

This page was built for publication: The universal exponentiable arrow