Sikkel: Multimode Simple Type Theory as an Agda Library

TL;DR

Sikkel is an Agda library that facilitates programming with extended type theories, supporting various extensions like guarded recursion and parametricity through a flexible, sound, and embeddable framework.

Contribution

It introduces a deeply embedded, extensible type theory library in Agda with a sound type checker based on presheaf models, enabling easier experimentation with extended type theories.

Findings

Supports multiple extended type theories like guarded recursion and parametricity

Ensures soundness through translation to presheaf model semantics

Allows combining different base categories via modalities

Abstract

Many variants of type theory extend a basic theory with additional primitives or properties like univalence, guarded recursion or parametricity, to enable constructions or proofs that would be harder or impossible to do in the original theory. However, implementing such extended type theories (either from scratch or by modifying an existing implementation) is a big hurdle for their wider adoption. In this paper we present Sikkel, a library in the dependently typed programming language Agda that allows users to program in extended type theories. It uses a deeply embedded language that can be easily extended with additional type and term constructors, thus supporting a wide variety of type theories. Moreover, Sikkel has a type checker that is sound by construction in the sense that all well-typed programs are automatically translated to their semantics in a shallow embedding based on presheaf models. Additionally, our model supports combining different base categories by using modalities to transport definitions between them. This enables in particular a general approach for extracting definitions to the meta-level, so that we can use the extended type theories to define regular Agda functions and prove properties of them. In this paper, we demonstrate Sikkel theories with guarded recursion and parametricity, but other extensions can be easily plugged in. For now, Sikkel supports only simple type theories but its model already anticipates the future addition of dependent types and a universe.