This is the root for accessing the Agda modules that accompany the paper How functorial are (deep) GADTs?. You can navigate through the files by just clicking on the names of the various modules.

The algorithm

In this module, we implement the algorithm adm presented informally in the paper.

open import map

Examples of the paper

The following modules implement the examples of the paper, introduced in Section 2 and treated in full detail in Section 4.

open import ex4-1
open import ex4-2
open import ex4-3
open import ex4-4
open import ex4-5

Further examples

The following modules implement data types and terms that exemplify some aspects of the algorithm that are only hinted at in the paper.

open import rose-deep
open import mutual-rec
open import deep-by-inst
open import deep-gadt-spec

Some basic data types

All the above examples rely on data types that need to be defined in our toy language, as done in the following modules.

open import list
open import bool
open import nat
open import rose
open import seq
open import G
open import phantomNat
open import even-odd
open import ptree
open import bush