English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We argue that locally Cartesian closed categories form a suitable doctrinefor defining dependent type theories, including non-extensional ones. Using thetheory of sketches, one may define syntactic categories for type theories in astyle that resembles the use of Martin-L\"of's Logical Framework, following the"judgments as types" principle. The concentration of type theories into theirlocally Cartesian closed categories of judgments is particularly convenient forproving syntactic metatheorems by semantic means (canonicity, normalization,etc.). Perhaps surprisingly, the notion of a context plays no role in thedefinitions of type theories in this sense, but the structure of a class ofdisplay maps can be imposed on a theory post facto wherever needed, asadvocated by the Edinburgh school and realized by the %worlds declarations ofthe Twelf proof assistant.  Uemura has proposed representable map categories together with a stratifiedlogical framework for similar purposes. The stratification in Uemura'sframework restricts the use of dependent products to be strictly positive, incontrast to the tradition of Martin-L\"of's logical framework andSchroeder-Heister's analysis of higher-level deductions. We prove a semanticadequacy result for locally Cartesian closed categories relative to Uemura'srepresentable map categories: if a theory is definable in the framework ofUemura, the locally Cartesian closed category that it generates is aconservative (fully faithful) extension of its syntactic representable mapcategory. On this basis, we argue for the use of locally Cartesian closedcategories as a simpler alternative to Uemura's representable map categories.

Syntactic categories for dependent type theory: sketching and adequacy