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:

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:

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:


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↩︎

  2. https://github.com/yoricksijsling/ornaments-thesis↩︎