A little (messy!) example of parametricity in cubical agda …

Parametricity-commentary.md

Commentary on Parametricity

copied from Slack thread, let me know if you have questions!

Background on parametricity

This was mostly based on Reynold’s original paper on parametricity, if I recall correctly …

In most proof assistants, you can’t prove that all functions are parametric, even if you can’t intuitionistically write a function that violates it (in particular, in the absence of LEM).

So you can’t prove that the type ∀ A → (A → (A → A) → A) is equivalent to the natural numbers, you actually have to define a sigma type of functions that are parametric (and you also have to quotient this by proofs of parametricity, I think), and then you can obtain your result.

The big downside is that this proof of parametricity is not universe-level polymorphic, so it works only up to some level! And you don’t know that the proof of parametricity is parametric itself. It’s very annoying.

In principle, though, it works well enough to take assumptions of parametricity, and the proof of parametricity for any particular function should be straight-forward.

But first we have to actually say what it means to be parametric …

How to define the shape of parametricity

The idea is that R×, R→, and R∀ define the shapes of parametricity …

… R∀ says in particular that it “preserves all relations” (∀ (X Y : Type ℓ) → ∀ (Rel : X → Y → Type ℓ′) → …) – once you define what that means for the stuff inside, of course

… and a function preserves relations when it takes related inputs to related outputs (R→)

So, for the natural numbers of shape A -> (A -> A) -> A, you get a relation R R→ (R R→ R) R→ R (for any relation R that relates two types)

… this means that when you prove two inputs z1, z2 are related by R, and that the inputs s1, s2 take inputs related by R to outputs also related by R, you get that the outputs f _ z1 s1 and f _ z2 s2 are also related by R.

And for the identity function A -> A, it’s pretty simple: R R→ R, any relation on the input is maintained for the output.

How to use parametricity

The proof that a particular function is parametric is pretty straightforward I think. Making use of it is a little trickier …

For a parametric function f .fst : ∀ A → (A → A) with the shape of the identity function, the parametricity proof f .snd simply says that that whatever relation the input satisfies, the output must also satisfy that relation …

… in particular, if the input is equal to a, the output must also be equal to a!

For something like f .fst : ∀ A → (A → A → A), you could pick a relation that says it is either equal to the first input or the second input. Thus for finite types you can simply enumerate the possibilities, prove that the inputs each are one of the possibilities, and then know that the output is one of those possibilites (and so, one of the inputs).

But for f .fst : ∀ A → (A → (A → A) → A) it is a little trickier, since we know this is equivalent to the natural numbers, which are infinite!

So what we do is we ask parametricity to tell us that what happens for an arbitrary element x : X (of an arbitrary type) is in fact determined by what happens for some n : ℕ of a known type.

We obtain a natural number that characterizes the function in the usual way – in particular, this is f .fst ℕ 0 (+1) (roughly) – and then we “guess” what f .fst X z s should be based on this natural number: itr n z s, we just iteratively apply s to z, n times.

In terms of relations, we say that a natural number n : ℕ is related to the output x : X when itr n z s ≡ x. And by definition of itr, 0 is related to z and when n is related to x then n+1 is related to s x.

So parametricity tells us that itr (f .fst ℕ 0 (+1)) z s ≡ f .fst X z s. What happens at ℕ determines what happens at any other type!

In particular, if f .fst ℕ = λ z s → z (known type) then f .fst X = λ z s → z (arbitrary type) as well, and so on for λ z s → s z and λ z s → s (s z) &c. by induction.

Thus f does exactly what we expect, and there are no surprises lurking beneath the forall.

Parametricity.agda

{-# OPTIONS --cubical --safe #-}
module Cubical.Parametricity where

open import Cubical.Core.Everything

open import Cubical.Data.Sigma.Properties
open import Cubical.Foundations.Everything
open import Cubical.Data.Nat
open import Cubical.Data.Prod
open import Cubical.Data.Empty

open import Cubical.HITs.SetQuotients renaming ([_] to ⟦_⟧)
open import Cubical.HITs.SetTruncation
open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.DecidableEq
open Iso

private
  variable
    ℓ ℓ′ ℓ′′ ℓ′′′ : Level

-- Universe-polymorphic Unit
data Singleton {ℓ : Level} : Type ℓ where
  triv : Singleton

-- A function that takes n arguments of a type and returns the same type
narg : (n : ℕ) → Type ℓ → Type ℓ
narg zero T = T
narg (suc n) T = (T → narg n T)

-- A tuple of n arguments of the same type (just a more ergonomic vector)
nprod : (n : ℕ) → Type ℓ → Type ℓ
nprod zero _ = Singleton
nprod (suc zero) T = T
nprod (suc (suc n)) T = (T × nprod (suc n) T)

-- Convert a n-tuple of types into the type of n-tuples of each type
↓n : {n : ℕ} → nprod n (Type ℓ) → Type ℓ
↓n {n = zero} _ = Singleton
↓n {n = suc zero} T = T
↓n {n = suc (suc n)} (T , Tn) = (T × ↓n {n = suc n} Tn)

-- Apply narg to nprod
ncurry : {n : ℕ} → {T : Type ℓ} → narg n T → nprod n T → T
ncurry {n = zero} r _ = r
ncurry {n = suc zero} f a = f a
ncurry {n = suc (suc n)} f (a , as) = ncurry {n = suc n} (f a) as

-- A relation generalized over types and type-level functions
record NRelated (n : ℕ) (ℓ ℓ′ : Level) : Type (ℓ-suc (ℓ-max ℓ ℓ′)) where
  constructor NRelate
  field
    -- Transform n types into a result type
    Tn : narg n (Type ℓ)
    -- Transform n relations into a resultant relation over their result type
    Rn : ∀ {X Y : nprod n (Type ℓ)} → (↓n X → ↓n Y → Type ℓ′) → (ncurry Tn X → ncurry Tn Y → Type ℓ′)

open NRelated

-- Easier way to apply a relation from NRelated 0
R0 : (NR : NRelated 0 ℓ ℓ′) → Tn NR → Tn NR → Type ℓ′
R0 NR = Rn NR {X = triv} {Y = triv} (λ _ _ → Singleton)

-- A relation over product types
_R×_ :
  {X1 Y1 : Type ℓ} → (R1 : X1 → Y1 → Type ℓ′) →
  {X2 Y2 : Type ℓ′′} → (R2 : X2 → Y2 → Type ℓ′′′) →
  X1 × X2 → Y1 × Y2 → Type (ℓ-max ℓ′ ℓ′′′)
_R×_ R1 R2 =
  (λ l r → R1 (proj₁ l) (proj₁ r) × R2 (proj₂ l) (proj₂ r))

infixr 20 _R→_

-- A relation over function types
_R→_ :
  {X1 Y1 : Type ℓ} → (R1 : X1 → Y1 → Type ℓ′) →
  {X2 Y2 : Type ℓ′′} → (R2 : X2 → Y2 → Type ℓ′′′) →
  (X1 → X2) → (Y1 → Y2) → Type (ℓ-max ℓ (ℓ-max ℓ′ ℓ′′′))
_R→_ R1 R2 =
  (λ f1 f2 → ∀ x1 x2 → (R1 x1 x2 → R2 (f1 x1) (f2 x2)))

RecF : (Type ℓ → Type ℓ) → (Type ℓ → Type ℓ)
RecF F X = (F X → X) → X

All : (Type ℓ → Type ℓ) → Type (ℓ-suc ℓ)
All {ℓ = ℓ} F = ∀ (X : Type ℓ) → F X

-- A relation on polymorphic functions, from a relation-functor for its functor
R∀ : NRelated 1 ℓ ℓ′ → NRelated 0 (ℓ-suc ℓ) (ℓ-suc (ℓ-max ℓ ℓ′))
R∀ {ℓ = ℓ} {ℓ′ = ℓ′} FR =
  NRelate (All (FR .Tn))
    (λ _ f g →
      ∀ (X Y : Type ℓ) →
      ∀ (Rel : X → Y → Type ℓ′) →
        FR .Rn Rel (f X) (g Y)
    )

-- Is the function parametric?
isParametric : (FR : NRelated 1 ℓ ℓ′) → (f : All (FR .Tn)) → Type (ℓ-suc (ℓ-max ℓ ℓ′))
isParametric FR f = R0 (R∀ FR) f f

-- Sigma type of parametric functions
Parametric : (FR : NRelated 1 ℓ ℓ′) → Type (ℓ-suc (ℓ-max ℓ ℓ′))
Parametric FR = Σ[ f ∈ All (FR .Tn) ] (isParametric FR f)

-- Set-quotient of Parametric by function equality, so the proof of parametricity
-- does not influence it.
ParametricFn : (FR : NRelated 1 ℓ ℓ′) → Type (ℓ-suc (ℓ-max ℓ ℓ′))
ParametricFn FR = Parametric FR / λ f g → f .fst ≡ g .fst

-- Obtain the function from a ParametricFn
fn :
    {FR : NRelated 1 ℓ ℓ′} →
    (∀ (X : Type ℓ) → isSet X → isSet (FR .Tn X)) →
    ParametricFn FR →
    ∀ (X : Type ℓ) → isSet X → FR .Tn X
fn _ ⟦ f ⟧ X _ = f .fst X
fn _ (eq/ a b r i) X _ = r i _
fn {FR = FR} squashing (squash/ x y p q i j) X squashed =
  isOfHLevel→isOfHLevelDep 2
    (λ _ → squashing X squashed)
    (g x) (g y) (cong g p) (cong g q)
    (squash/ x y p q) i j
    where
      g : ParametricFn FR → FR .Tn X
      g e = fn {FR = FR} squashing e X squashed

-- The functor that characterizes the algebra of the natural numbers
ℕF : Type ℓ → Type ℓ
ℕF X = X → (X → X) → X

ℕFset : ∀ (X : Type ℓ) → isSet X → isSet (ℕF X)
ℕFset X set = isSetΠ λ _ → isSetΠ λ _ → set

-- The relation-functor
ℕFR : {X Y : Type ℓ} → (R : X → Y → Type ℓ′) → ℕF X → ℕF Y → Type (ℓ-max ℓ ℓ′)
ℕFR R = R R→ (R R→ R) R→ R

ℕFR1 : NRelated 1 ℓ (ℓ-max ℓ ℓ′)
ℕFR1 = NRelate ℕF ℕFR

Pℕ′ : Type (ℓ-suc (ℓ-max ℓ ℓ′))
Pℕ′ {ℓ = ℓ} {ℓ′ = ℓ′} = Parametric {ℓ = ℓ} (ℕFR1 {ℓ = ℓ} {ℓ′ = ℓ′})

Pℕ : Type (ℓ-suc (ℓ-max ℓ ℓ′))
Pℕ {ℓ = ℓ} {ℓ′ = ℓ′} = ParametricFn {ℓ = ℓ} (ℕFR1 {ℓ = ℓ} {ℓ′ = ℓ′})

-- Universe-polymorphic natural numbers
data ℓℕ {ℓ : Level} : Type ℓ where
  zer0 : ℓℕ
  sucr : ℓℕ {ℓ = ℓ} → ℓℕ

induction : {P : ℓℕ {ℓ = ℓ′} → Type ℓ} → (n : ℓℕ) → P zer0 → (∀ m → P m → P (sucr m)) → P n
induction zer0 z _ = z
induction (sucr n) z s = s n (induction n z s)

-- This characterizes the expected parametric functions
itr : {A : Type ℓ′} → ℓℕ {ℓ = ℓ} → A → (A → A) → A
itr zer0 z _ = z
itr (sucr n) z s = s (itr n z s)

-- Proof that it is parametric
itrparam : ∀ (n : ℓℕ {ℓ = ℓ}) → (X Y : Type ℓ) → (Rel : X → Y → Type (ℓ-max ℓ ℓ′)) →
  ℕFR1 {ℓ = ℓ} {ℓ′ = ℓ′} .Rn Rel (itr n) (itr n)
itrparam n X Y Rel = λ p q pq x y xy →
  induction n pq (λ m → xy (itr m p x) (itr m q y))

itrself : ∀ {ℓ ℓ′} → (n : ℓℕ {ℓ = ℓ}) →
  itr {ℓ = ℓ′} (itr n zer0 sucr) zer0 sucr ≡ n
itrself zer0 = refl
itrself {ℓ′ = ℓ′} (sucr n) i = sucr (itrself {ℓ′ = ℓ′} n i)

injSucr : ∀ {n m : ℓℕ {ℓ = ℓ}} → sucr n ≡ sucr m → n ≡ m
injSucr eq = cong predSucr eq where
  predSucr : ℓℕ → ℓℕ
  predSucr zer0 = zer0
  predSucr (sucr n) = n

discreteℓℕ : Discrete (ℓℕ {ℓ = ℓ})
discreteℓℕ zer0 zer0 = yes refl
discreteℓℕ zer0 (sucr n) = no λ eq -> subst (λ { zer0 → ℓℕ ; (sucr _) → ⊥ }) eq zer0
discreteℓℕ (sucr m) zer0 = no λ eq -> subst (λ { zer0 → ⊥ ; (sucr _) → ℓℕ }) eq zer0
discreteℓℕ (sucr m) (sucr n) with discreteℓℕ m n
... | yes p = yes (cong sucr p)
... | no p = no (λ x → p (injSucr x))

{-
Pℕ′→ℕ : Pℕ′ {ℓ = ℓ} {ℓ′ = ℓ′} → ℓℕ {ℓ = ℓ}
Pℕ′→ℕ p = p .fst ℓℕ zer0 sucr

ℕ→Pℕ′ : ℓℕ → Pℕ′ {ℓ = ℓ} {ℓ′ = ℓ′}
ℕ→Pℕ′ {ℓ = ℓ} {ℓ′ = ℓ′} n = (λ X → itr n) , (itrparam {ℓ = ℓ} {ℓ′ = ℓ′} n)

ℕ→ℕ′ : (n : ℓℕ {ℓ = ℓ}) → Pℕ′→ℕ {ℓ = ℓ} {ℓ′ = ℓ′} (ℕ→Pℕ′ {ℓ = ℓ} {ℓ′ = ℓ′} n) ≡ n
ℕ→ℕ′ zer0 i = zer0
ℕ→ℕ′ {ℓ = ℓ} {ℓ′ = ℓ′} (sucr n) i = sucr (ℕ→ℕ′ {ℓ = ℓ} {ℓ′ = ℓ′} n i)

-- We cannot prove that ℕ→Pℕ′ (Pℕ′→ℕ f) ≡ f, since the proofs of parametricity
-- may be different, so we instead prove that the functions are equal.
-- Note: applying funExt saves us one universe level in ℓ′
Pℕ′→Pℕ′ : ∀ f → ℕ→Pℕ′ {ℓ = ℓ} {ℓ′ = ℓ} (Pℕ′→ℕ {ℓ = ℓ} {ℓ′ = ℓ} f) .fst ≡ f .fst
Pℕ′→Pℕ′ f = funExt λ X → funExt λ z → funExt λ s →
  -- The relation says if Pℕ→ℕ f ↦ n, then f z s ↦ x
  f .snd ℓℕ X (λ n x → itr n z s ≡ x)
  zer0 z refl
  sucr s (λ n x p i → s (p i))
-}

ℕ→Pℕ : ℓℕ {ℓ = ℓ} → Pℕ {ℓ = ℓ} {ℓ′ = ℓ′}
ℕ→Pℕ {ℓ = ℓ} {ℓ′ = ℓ′} n = ⟦ (λ X → itr n) , (itrparam {ℓ = ℓ} {ℓ′ = ℓ′} n) ⟧

Pℕ→ℕ : Pℕ {ℓ = ℓ} {ℓ′ = ℓ′} → ℓℕ {ℓ = ℓ}
Pℕ→ℕ {ℓ = ℓ} {ℓ′ = ℓ′} f = fn {FR = ℕFR1 {ℓ = ℓ} {ℓ′ = ℓ′}} ℕFset
  f ℓℕ (Discrete→isSet discreteℓℕ) zer0 sucr

ℕ→ℕ : (n : ℓℕ {ℓ = ℓ}) → Pℕ→ℕ {ℓ = ℓ} {ℓ′ = ℓ′} (ℕ→Pℕ {ℓ = ℓ} {ℓ′ = ℓ′} n) ≡ n
ℕ→ℕ zer0 i = zer0
ℕ→ℕ {ℓ = ℓ} {ℓ′ = ℓ′} (sucr n) i = sucr (ℕ→ℕ {ℓ = ℓ} {ℓ′ = ℓ′} n i)

Pℕ→Pℕ : ∀ f → ℕ→Pℕ {ℓ = ℓ} {ℓ′ = ℓ} (Pℕ→ℕ {ℓ = ℓ} {ℓ′ = ℓ} f) ≡ f
Pℕ→Pℕ = elimProp (λ _ → squash/ _ _) λ f → eq/ _ _
  ( funExt λ X → funExt λ z → funExt λ s →
    -- The relation says if Pℕ→ℕ f ↦ n, then f z s ↦ x
    f .snd ℓℕ X (λ n x → itr n z s ≡ x)
    zer0 z refl
    sucr s (λ n x p i → s (p i))
  )

-- This is the direct iso we proved, but they live in different universes
-- Pℕ {ℓ = ℓ} {ℓ′ = ℓ} : Type (ℓ-suc ℓ)
-- ℓℕ {ℓ = ℓ} : Type ℓ
-- so they cannot be compared with ≡
Pℕ≅ℓℕ : Iso (Pℕ {ℓ = ℓ} {ℓ′ = ℓ}) (ℓℕ {ℓ = ℓ})
Pℕ≅ℓℕ {ℓ = ℓ} = (iso (Pℕ→ℕ {ℓ = ℓ} {ℓ′ = ℓ}) (ℕ→Pℕ {ℓ = ℓ} {ℓ′ = ℓ}) (ℕ→ℕ {ℓ′ = ℓ}) Pℕ→Pℕ)

lifting : ∀ {T : Type ℓ} → Iso T (Lift {j = ℓ′} T)
lifting = iso lift lower (λ _ → refl) (λ _ → refl)

-- But of course ℓℕ is the same in every universe
liftingℓℕ : Iso (ℓℕ {ℓ = ℓ}) (ℓℕ {ℓ = ℓ′})
liftingℓℕ = iso
  (λ n → itr n zer0 sucr)
  (λ m → itr m zer0 sucr)
  itrself itrself

-- So Pℕ *is* the natural numbers, albeit one level higher
Pℕ≡ℓℕ : Pℕ {ℓ = ℓ} {ℓ′ = ℓ} ≡ ℓℕ {ℓ = ℓ-suc ℓ}
Pℕ≡ℓℕ = isoToPath (compIso Pℕ≅ℓℕ liftingℓℕ)

Updated to work with Agda version 2.6.1 and cubical library v0.2.