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 describe the categorical semantics for a simply typed variant and asimplified dependently typed variant of Cocon, a contextual modal type theorywhere the box modality mediates between the weak function space that is used torepresent higher-order abstract syntax (HOAS) trees and the strong functionspace that describes (recursive) computations about them. What makes Cocondifferent from standard type theories is the presence of first-class contextsand contextual objects to describe syntax trees that are closed with respect toa given context of assumptions. Following M. Hofmann's work, we use a presheafmodel to characterise HOAS trees. Surprisingly, this model already provides thenecessary structure to also model Cocon. In particular, we can capture thecontextual objects of Cocon using a comonad $\flat$ that restricts presheavesto their closed elements. This gives a simple semantic characterisation of theinvariants of contextual types (e.g. substitution invariance) and identifiesCocon as a type-theoretic syntax of presheaf models. We further extend thischaracterisation to dependent types using categories with families and showthat we can model a fragment of Cocon without recursor in the Fitch-styledependent modal type theory presented by Birkedal et. al..

A Category Theoretic View of Contextual Types: from Simple Types to Dependent Types