# Parametricity for described datatypes

View source

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 _∘_ id : {A : Set} → A → A id x = x const : {A : Set} → A → {B : Set} → B → A const x _ = x _$_ : {A : Set} {P : A → Set} (f : ∀ x → P x) (x : A) → P x
f x = f x _×_ : (A B : Set) → Set A × B = Σ A (const B) case_of_ : {A : Set} {P : A → Set} (x : A) → ((x : A) → P x) → P x case x of f = f x _∘_ : {A : Set} {P : A → Set} {Q : {x : A} → P x → Set} (g : {x : A} → (y : P x) → Q y) (f : (x : A) → P x) → (x : A) → Q (f x) _∘_ g f x = g (f x) data Fin : Nat → Set where zero : ∀ {n} → Fin (suc n) suc : ∀ {n} → Fin n → Fin (suc n) data Vec (A : Set) : Nat → Set where [] : Vec A 0 _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n) lookup : {A : Set} {n : Nat} → Vec A n → Fin n → A lookup (x ∷ _) zero = x lookup (_ ∷ xs) (suc n) = lookup xs n map : (A → B) → {n : Nat} → Vec A n → Vec B n map f [] = [] map f (x ∷ xs) = f x ∷ map f xs iter : {n : Nat} → (Fin n → A) → Vec A n iter {n = zero } f = [] iter {n = suc n} f = f zero ∷ iter (f ∘ suc) Rel : Set → Set → Set Rel A B = A → B → Set data All (P : A → Set) : List A → Set where [] : All P [] _∷_ : ∀ {x} → P x → ∀ {xs} → All P xs → All P (x ∷ xs) # A universe of descriptions The first step is to equip ourselves with a universe of descriptions to encode inductive indexed datatypes. See the work from Pierre-Evariste Dagand1 to learn about descriptions. The one chosen here is an extension of Yorick Sijsling’s2, with some additions: • indices now depend on the parameters; • recursive occurences can have different parameters. Actually I removed this for the time being, since it’s not really important for what we are trying to achieve. Still, can be done. ## Encoding telescopes 🔭 So we begin by defining an encoding of telescopes to encode the parameters and indices of datatypes. I just found out it is very similar to what is introduced in [Akaposi2015]. What we are apparently doing is adding telescopes and telescope substitutions in our theory, whereas they leave them outside of types. In summary, we define the type of telescopes parametrized by some set A. And given a telescope, and an element of A, we define the type of telescope substitutions: \gdef\set{\textsf{Set}} \gdef\tele#1{\textsf{Tele}\ #1} \gdef\rel#1#2{\textsf{Rel}\ #1\ #2}\begin{aligned} A : \set\ &⊢\ \tele A : \set \\ A : \set,\ Ω : \tele A,\ x : A\ &⊢ ⟦ Ω ⟧\ x \ : \set \end{aligned} For our purposes, a telescope substitution is a huge Σ-type containing an element for every type in the telescope. We can introduce empty telescopes or extend them by the right. \frac{}{A : \set \ ⊢\ ε : \tele A} \quad \frac {A : \set,\ Ω : \tele A,\ ⊢\ F : Σ\ A\ ⟦ Ω ⟧ → \set} {A : \set,\ Ω : \tele A\ ⊢\ Ω\ ▷\ F : \tele A} infixl 1 _▷_ _▷₀_ data Tele (A : Set) : Set ⟦_⟧ : {A : Set} → Tele A → A → Set data Tele A where ε : Tele A _▷_ : (T : Tele A) → (Σ A ⟦ T ⟧ → Set) → Tele A ⟦ ε ⟧ x = ⊤ ⟦ T ▷ F ⟧ x = Σ (⟦ T ⟧ x) (F ∘ (x ,_)) _▷₀_ : {A : Set} (T : Tele A) (B : Set) → Tele A T ▷₀ B = T ▷ const B Because telescopes are parametrized by some Set, we can define a telescope that depend on the telescope substitution of another telescope. That’s how we encode parameters-dependent indices. Describing the parameters and indices of a datatype boils down to exhibiting some P and I such that P : Tele ⊤ and I : Tele (⟦ T ⟧ tt). We too can extend telescopes with telescopes. For our purposes, it only makes sense to extend non-parametrized telescopes: \begin{aligned} Ω : \tele ⊤,\ Ω' : \tele (⟦ Ω ⟧\ tt)\ &⊢ \textsf{extend}\ Ω' : \tele ⊤ \\ Ω : \tele ⊤,\ Ω' : \tele (⟦ Ω ⟧\ tt)\ &⊢ \textsf{pr}\ : ⟦ \textsf{extend}\ Ω' ⟧\ tt → Σ\ (⟦ Ω ⟧\ tt)\ ⟦ Ω' ⟧ \end{aligned} ExTele : Tele ⊤ → Set ExTele T = Tele (⟦ T ⟧ tt) Ctx : {T : Tele ⊤} → ExTele T → Set Ctx Γ = Σ _ ⟦ Γ ⟧ extend : {T : Tele ⊤} → ExTele T → Tele ⊤ pr : {T : Tele ⊤} {Γ : ExTele T} → ⟦ extend Γ ⟧ tt → Ctx Γ extend {T} ε = T extend (G ▷ F) = extend G ▷ F ∘ pr ∘ snd pr {Γ = ε} γ = γ , tt pr {Γ = Γ ▷ F} (γ′ , x) = let (t , γ) = pr γ′ in t , γ , x ## Constructors Like Yorick we describe constructors first and datatypes second by giving a vector of constructor descriptions. This has the benefit of following more closely the structure of Agda datatypes: data ConDesc {P : Tele ⊤} (Γ I : ExTele P) : Set Both the constructor’s current context Γ and its indices I are extensions of the datatype parameters. The rest is pretty standard: • κ marks the end of a constructor. We simply compute indices from the current context. • ι marks the position of a recursive occurence. Here we provide indices computed from the context. I am saddened by the fact that this recursive occurence is not added to the context of the rest of the constructor. This can probably be done but would require too much effort for what it’s worth. Who does that anyway? • σ marks the introduction of a variable. Its type is computed from the local context, and the variable is added to the context for the rest of the constructor. data ConDesc {P} Γ I where κ : (f : (γ : Ctx Γ) → ⟦ I ⟧ (γ .fst)) → ConDesc Γ I ι : (f : (γ : Ctx Γ) → ⟦ I ⟧ (γ .fst)) → ConDesc Γ I → ConDesc Γ I σ : (S : Ctx Γ → Set ) → ConDesc (Γ ▷ S) I → ConDesc Γ I ⟦_⟧ᶜ : {P : Tele ⊤} {Γ I : ExTele P} (C : ConDesc Γ I) → (Ctx I → Set) → (Σ (⟦ P ⟧ tt) (λ p → ⟦ Γ ⟧ p × ⟦ I ⟧ p) → Set) ⟦ κ f ⟧ᶜ X (p , γ , i) = f (p , γ) ≡ i ⟦ ι f C ⟧ᶜ X g@(p , γ , _) = X (p , f (p , γ)) × ⟦ C ⟧ᶜ X g ⟦ σ S C ⟧ᶜ X (p , γ , i) = Σ (S (p , γ)) λ s → ⟦ C ⟧ᶜ X (p , (γ , s) , i) ## Datatypes Moving on, we encode datatypes as a vector of constructor descriptions that share the same parameters and indices telescopes. Then we tie the knot: Desc : (P : Tele ⊤) (I : ExTele P) → Nat → Set Desc P I n = Vec (ConDesc ε I) n ⟦_⟧ᵈ : {P : Tele ⊤} {I : ExTele P} {n : Nat} (D : Desc P I n) → (Ctx I → Set) → (Ctx I → Set) ⟦_⟧ᵈ {n = n} D X (p , i) = Σ (Fin n) λ k → ⟦ lookup D k ⟧ᶜ X (p , tt , i) data μ {n} {P : Tele ⊤} {I : ExTele P} (D : Desc P I n) (pi : Ctx I) : Set where ⟨_⟩ : ⟦ D ⟧ᵈ (μ D) pi → μ D pi We can also define some helper constr to easily retrieve the k th constructor from a description: module _ {P : Tele ⊤} {I : Tele (⟦ P ⟧ tt)} {n : Nat} (D : Desc P I n) where Constr′ : {Γ : Tele (⟦ P ⟧ tt)} → ConDesc Γ I → Ctx Γ → Set Constr′ (κ f ) pg = μ D (fst pg , f pg) Constr′ (ι f C) pg = μ D (fst pg , f pg) → Constr′ C pg Constr′ (σ S C) (p , γ) = (s : S (p , γ)) → Constr′ C (p , γ , s) module _ {C′ : ConDesc ε I} (mk : {(p , i) : Ctx I} → ⟦ C′ ⟧ᶜ (μ D) (p , tt , i) → μ D (p , i)) where constr′ : {Γ : Tele (⟦ P ⟧ tt)} (C : ConDesc Γ I) ((p , γ) : Ctx Γ) → ({i : ⟦ I ⟧ p} → ⟦ C ⟧ᶜ (μ D) (p , γ , i) → ⟦ C′ ⟧ᶜ (μ D) (p , tt , i)) → Constr′ C (p , γ) constr′ (κ f ) pg tie = mk (tie refl) constr′ (ι f C) pg tie x = constr′ C pg (tie ∘ (x ,_)) constr′ (σ S C) (p , γ) tie s = constr′ C (p , γ , s) (tie ∘ (s ,_)) -- | type of the kth constructor Constr : (k : Fin n) (p : ⟦ P ⟧ tt) → Set Constr k p = Constr′ (lookup D k) (p , tt) -- | kth constructor constr : (k : Fin n) (p : ⟦ P ⟧ tt) → Constr k p constr k p = constr′ (λ x → ⟨ k , x ⟩) (lookup D k) (p , tt) id Another useful operation is to retrieve a telescope for every constructor of datatype. module _ {P : Tele ⊤} {I : ExTele P} (X : Ctx I → Set) where contotele′ : {Γ : ExTele P} → ConDesc Γ I → (T : ExTele P) → (((p , γ) : Ctx T) → ⟦ Γ ⟧ p) → ExTele P contotele′ (κ _) T mk = T contotele′ (ι f C) T mk = contotele′ C (T ▷ λ (p , γ) → X (p , f (p , mk (p , γ)))) λ (p , γ , x) → mk (p , γ) contotele′ (σ S C) T mk = contotele′ C (T ▷ λ (p , γ) → S (p , (mk (p , γ)))) λ (p , γ , s) → (mk (p , γ)) , s contotele : {P : Tele ⊤} {I : ExTele P} {n : Nat} → Desc P I n → Fin n → ExTele P contotele D k = contotele′ (μ D) (lookup D k) ε (const tt) ## Examples Some examples to reassure ourselves as to whether it works as intended: module Examples where natD : Desc ε ε 2 natD = κ (const tt) ∷ ι (const tt) (κ (const tt)) ∷ [] nat : Set nat = μ natD (tt , tt) ze : Constr natD zero tt ze = constr natD zero tt su : Constr natD (suc zero) tt su = constr natD (suc zero) tt vecD : Desc (ε ▷₀ Set) (ε ▷₀ nat) 2 vecD = κ (const (tt , ze)) ∷ σ (const nat) (σ (λ (p , _) → p .snd) (ι (λ (p , ((tt , n) , x )) → tt , n) (κ (λ (_ , ((tt , n) , _)) → tt , (su n))))) ∷ [] vec : (A : Set) → nat → Set vec A n = μ vecD ((tt , A) , tt , n) nil : {A : Set} → Constr vecD zero (tt , A) nil {A} = constr vecD zero (tt , A) cons : {A : Set} → Constr vecD (suc zero) (tt , A) cons {A} = constr vecD (suc zero) (tt , A) xs : vec nat (su (su ze)) xs = cons _ (su ze) (cons _ (su (su ze)) nil) So far so good. Let’s move to the fun part, we’re in for the big bucks. # From descriptions to descriptions To keep our goal in sight, here is what should happen for lists: module Translation where module Goal where listD : Desc (ε ▷ const Set) ε 2 listD = κ (const tt) ∷ σ (λ ((tt , A) , γ) → A) (ι (λ (p , γ) → tt) (κ (const tt))) ∷ [] list : Set → Set list A = μ listD ((tt , A) , tt) nil : {A : Set} → list A nil {A} = ⟨ zero , refl ⟩ cons : {A : Set} → A → list A → list A cons x xs = ⟨ suc zero , x , xs , refl ⟩ -- the following is the description we want to derive -- listᵣD : Desc (ε ▷₀ Set ▷₀ Set ▷ λ (tt , (tt , A) , B) → Rel A B) -- (ε ▷ (λ ((((_ , A) , B) , R) , tt) → list A) -- ▷ (λ ((((_ , A) , B) , R) , tt , _) → list B)) 2 -- listᵣD = κ (λ ((((tt , A) , B) , R) , tt) → (tt , nil) , nil) -- ∷ ( σ (λ (((( A) , B) , R) , tt) → A ) -- σ (λ ((((tt , A) , B) , R) , tt , _)         → B                           )
--          $σ (λ ((_ , R) , (tt , x) , y) → R x y ) --$ σ (λ ((((tt , A) , B ) , R) , _)             → list A                      )
--          $σ (λ ((((tt , A) , B ) , R) , _) → list B ) --$ ι (λ (γ , (_ , xs) , ys)                     → γ , (tt , xs) , ys          )
--          κ (λ (_ , (((((_ , x) , y) , _) , xs) , ys)) → (tt , cons x xs) , cons y ys) -- ) -- ∷ [] -- listᵣ : {A B : Set} (R : Rel A B) → list A → list B → Set -- listᵣ {A} {B} R xs ys = μ listᵣD ((((tt , A) , B) , R) , (tt , xs) , ys) -- nilᵣ : {A B : Set} {R : Rel A B} → listᵣ R nil nil -- nilᵣ = ⟨ zero , refl ⟩ -- consᵣ : {A B : Set} {R : Rel A B} -- → ∀ {x y } (x≈y : R x y) -- → ∀ {xs ys} (xs≈ys : listᵣ R xs ys) -- → listᵣ R (cons x xs) (cons y ys) -- consᵣ {x = x} {y} x≈y {xs} {ys} xs≈ys = -- ⟨ suc zero , x , y , x≈y , xs , ys , xs≈ys , refl ⟩ Hm. What we expect to generate looks like a mess. On a positive note it does seem like we do not need to add recursive occurences to the context. It is also reassuring that we can indeed encode the relation. Tbh the relation on its own is not that useful. What would be great is if we were able to derive the abstraction theorem for this datatype too: -- param : (R : Rel A A) (PA : ∀ x → R x x) -- → (xs : list A) → listᵣ R xs xs -- param R PA ⟨ zero , refl ⟩ = nilᵣ -- param R PA ⟨ suc zero , x , xs , refl ⟩ = consᵣ (PA x) (param R PA xs) This also looks quite doable. Moving forward while keeping our head down. ## Relating telescope substitutions The first thing we need is a relation on telescope substitutions. Naturally, because substitutions are encoded as Σ-types, two substitutions are related iff their elements are related one to one, using the relational interpretation of their respective types. T : \tele A,\ x_1 : A,\ x_2 : A,\ x_r : ⟦A⟧_p \ ⊢ ⟦Π\ A\ ⟦ T ⟧ ⟧_p\ x_1\ x_2\ x_r : \rel {(⟦ T ⟧\ x_1)} {(⟦ T ⟧\ x_2)} \begin{aligned} ⟦Π\ A\ ⟦ε⟧⟧_p\ x_1\ x_2\ x_r\ t_1\ t_2 &≡ ⊤ \\ ⟦Π\ A\ ⟦T\ ▷\ F⟧⟧_p\ x_1\ x_2\ x_r\ (t_1 , s_1)\ (t_2 , s_2) &≡ Σ\ (⟦Π\ A\ ⟦T⟧⟧_p\ x_1\ x_2\ x_r\ t_1\ t_2)\ λ\ t_r\ . \ ⟦ F ⟧_p\ t_1\ t_2\ t_r\ s_1\ s_2 \end{aligned} The only problem here is that we need ⟦A⟧_p and ⟦F⟧_p. We cannot possibly compute it, because A could be virtually anything, not just one of our friendly described datatypes. An easy way out is to kindly ask for these relations. Therefore we introduce a new type \textsf{Help}\ T associated with the telescope T we’re trying to translate, whose inhabitants must hold every required relation. Help : Tele A → A → A → Set -- I suspect we don't care about xᵣ so I'm omitting it ₜ⟦_⟧ₚ : (T : Tele A) {x y : A} → Help T x y → Rel (⟦ T ⟧ x) (⟦ T ⟧ y) Help ε _ _ = ⊤ Help (T ▷ F) x₁ x₂ = Σ (Help T x₁ x₂) λ H → ∀ t₁ t₂ (tᵣ : ₜ⟦ T ⟧ₚ H t₁ t₂) → Rel (F (x₁ , t₁)) (F (x₂ , t₂)) ₜ⟦ ε ⟧ₚ tt tt tt = ⊤ ₜ⟦ T ▷ F ⟧ₚ (H , HF) (t₁ , s₁) (t₂ , s₂) = Σ (ₜ⟦ T ⟧ₚ H t₁ t₂) λ tᵣ → HF t₁ t₂ tᵣ s₁ s₂ ExHelp : {P : Tele ⊤} → ExTele P → Set ExHelp I = ∀ p₁ p₂ → Help I p₁ p₂ ## Not my type Our relation will be inductively defined, so we need to figure out beforehand its parameters and indices. Parameters are easy, we expect two substitutions of the initial parameters’ telescope, and a proof that they are related. module _ {P : Tele ⊤} {I : ExTele P} {n : Nat} (D : Desc P I n) (HP : Help P tt tt) (HI : ExHelp I) where Pₚ : Tele ⊤ Pₚ = ε ▷₀ ⟦ P ⟧ tt ▷₀ ⟦ P ⟧ tt ▷ λ (_ , (_ , p₁) , p₂) → ₜ⟦ P ⟧ₚ HP p₁ p₂ p₁ : ⟦ Pₚ ⟧ tt → ⟦ P ⟧ tt p₁ (((_ , p) , _) , _) = p p₂ : ⟦ Pₚ ⟧ tt → ⟦ P ⟧ tt p₂ (((_ , _) , p) , _) = p Iₚ : ExTele Pₚ Iₚ = ε ▷ (λ ((((_ , p₁) , _) , _) , _) → ⟦ I ⟧ p₁) ▷ (λ ((((_ , _) , p₂) , _) , _) → ⟦ I ⟧ p₂) ▷ (λ ((((_ , p₁) , _) , _) , (_ , i₁) , _) → μ D (p₁ , i₁)) ▷ (λ ((((_ , _) , p₂) , _) , (_ , i₂) , _) → μ D (p₂ , i₂)) Apart from the typical clumsiness of dealing with substitutions, we have our parameters and indices. The only thing left is to translate constructors. For this, we walk through the constructors, carrying continuations for progressively constructing the two elements we are relating. Cₚ′ : {Γₚ : ExTele Pₚ} {Γ : ExTele P} → (C : ConDesc Γ I) -- | Left projection of the context → (c₁ : {p : ⟦ Pₚ ⟧ tt} → ⟦ Γₚ ⟧ p → ⟦ Γ ⟧ (p₁ p)) -- | Right projection of the context → (c₂ : {p : ⟦ Pₚ ⟧ tt} → ⟦ Γₚ ⟧ p → ⟦ Γ ⟧ (p₂ p)) -- | Builder of the left element → (f₁ : {p : ⟦ Pₚ ⟧ tt} {g : ⟦ Γₚ ⟧ p} {i : ⟦ I ⟧ (p₁ p)} → ⟦ C ⟧ᶜ (μ D) (p₁ p , c₁ g , i) → μ D (p₁ p , i)) -- | Builder of the right element → (f₂ : {p : ⟦ Pₚ ⟧ tt} {g : ⟦ Γₚ ⟧ p} {i : ⟦ I ⟧ (p₂ p)} → ⟦ C ⟧ᶜ (μ D) (p₂ p , c₂ g , i) → μ D (p₂ p , i)) → (ConDesc Γₚ Iₚ → ConDesc ε Iₚ) → ConDesc ε Iₚ Cₚ′ (κ f) c₁ c₂ f₁ f₂ tie = tie (κ (λ (p , g) → (((tt , ( f (p₁ p , c₁ g))) , f (p₂ p , c₂ g)) , f₁ refl) , f₂ refl)) Cₚ′ (ι f C) c₁ c₂ f₁ f₂ tie = Cₚ′ C (c₁ ∘ λ ((p , _) , _) → p) (c₂ ∘ λ ((p , _) , _) → p) (λ {_} {((_ , a) , _)} {_} C → f₁ (a , C)) (λ {_} {(_ , a)} {_} C → f₂ (a , C)) (tie ∘ λ C → σ (λ (p , g) → μ D (p₁ p , f (p₁ p , c₁ g))) σ (λ (p , g , _) → μ D (p₂ p , f (p₂ p , c₂ g)))
$ι (λ (p , (_ , x) , y) → (((tt , _) , _) , x) , y)$ C)

Cₚ′ (σ S C) c₁ c₂ f₁ f₂ tie =
Cₚ′ C
(λ (((g , s₁) , _) , _)  → c₁ g , s₁)
(λ (((g , _) , s₂) , _)  → c₂ g , s₂)
(λ {_} {(((_ , a), _) , _)} {_} C → f₁ (a , C))
(λ {_} {((_ , a) , _)} {_} C      → f₂ (a , C))
(tie ∘ λ C → σ (λ (p , g)     → S (p₁ p , c₁ g))
$σ (λ (p , g , _) → S (p₂ p , c₂ g))$ σ (λ (p , ((g , x), y)) → {!!})
-- we need some some relation here
-- that should be provided
\$ C)

Cₚ : Fin n → ConDesc ε Iₚ
Cₚ k = Cₚ′ (lookup D k) id id (⟨_⟩ ∘ (k ,_)) (⟨_⟩ ∘ (k ,_)) id

Dₚ : Desc Pₚ Iₚ n
Dₚ = iter Cₚ

CPS all the way.

Assuming we had implement what’s missing above, we would have the relation we wanted:

⟦_⟧ₚ : {p₁ p₂ : ⟦ P ⟧ tt} (pᵣ : ₜ⟦ P ⟧ₚ HP p₁ p₂)
{i₁ : ⟦ I ⟧ p₁} {i₂ : ⟦ I ⟧ p₂}
→ Rel (μ D (p₁ , i₁)) (μ D (p₂ , i₂))
⟦_⟧ₚ pᵣ t₁ t₂ = μ Dₚ ((_ , pᵣ) , (_ , t₁) , t₂)

The abstraction theorem becomes:

param′ : ∀ {k p i Γ γ}
{C : ConDesc Γ I}
(x : ⟦ C ⟧ᶜ (μ D) (p , γ , i))
(HP : ₜ⟦ P ⟧ₚ HP p p)
→ (mk : ⟦ C ⟧ᶜ (μ D) (p , γ , i) → ⟦ lookup D k ⟧ᶜ (μ D) (p , tt , i))
→ ⟦ lookup Dₚ k ⟧ᶜ (μ Dₚ) ((((tt , p) , p) , HP) , tt , ((((tt , i) , i)
, ⟨ k , mk x ⟩)
, ⟨ k , mk x ⟩))
param′ {C = κ f} x HP mk = {!!}
param′ {C = ι f C} x HP mk = {!!}
param′ {C = σ S C} x HP mk = {!!}

param : ∀ {p i} (t : μ D (p , i)) (RP : ₜ⟦ P ⟧ₚ HP p p) → ⟦_⟧ₚ RP t t
param ⟨ k , x ⟩ RP = ⟨ k , param′ x RP id ⟩

An exemple on lists:

# Conclusion

Now, why should we care? Well, I don’t really know just yet. I do think there is value in having such transformations implemented in a type-safe way. Still, because these representations are not intrinsic to how datatypes are defined in the theory, it make for a clumsy experience. Add the lack of cumulativity and everything becomes quite tedious.

Things I would like to explore next:

• Derive the proofs that any datatype and its constructors are univalently parametric. As of now we can derive the relation, what remains to be proven is deriving an equivalence (easy) and a proof that the two are equivalent.
• Get rid of the --type-in-type flag, using Effectfully’s technique, or embracing --cumulativity?
• Investigate encodings of other constructions: Co-inductive types? Records?
• Look into Formality’s encoding of datatypes and what it means for generic programming.

Akaposi2015
Towards cubical type theory
Thorsten Altenkirch, Ambrus Kaposi
https://akaposi.github.io/nominal.pdf
Bernardy2010
Parametricity and Dependent Types
Jean-Philippe Bernardy, Patrik Jansson, Ross Paterson
http://www.staff.city.ac.uk/~ross/papers/pts.pdf
Tabareau2019
The Marriage of Univalence and Parametricity
Nicolas Tabareau, Eric Tanter, Matthieu Sozeau
https://arxiv.org/pdf/1909.05027.pdf

1. In particular, his PhD thesis: Reusability and Dependent Types↩︎