Parametricity for described datatypes

Posted on .

This entry is just me figuring stuff out by writing it down. The goal is to derive automatically the logical relation generated by a datatype in Agda, without metaprogramming. Or, to be correct, without unsafe metaprogramming — no reflection allowed.

The title means nothing and this is WIP.

Only one thing to keep in mind: we are using the dirtiest of tricks, --type-in-type. For the time being, this will do just fine.

Prelude
{-# OPTIONS --type-in-type #-}

open import Agda.Primitive
open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality
open import Agda.Builtin.Nat
open import Agda.Builtin.List

variable A B : Set

infixr -1 _$_
infixl 2 _