An example of parametricity in cubical agda, proving ((X : Type) -> X -> (X -> X) -> X) == Nat

Parametricity.agda

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

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma.Properties
open import Cubical.Foundations.Everything
open import Cubical.Data.Everything hiding (Iso ; compIso)

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

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 =
  elimSquash₀ (λ _ → squashing X squashed) (squash/ x y p q)
              (g x) (g y) (cong g p) (cong g 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 = isSetPi λ _ → isSetPi λ _ → 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ℕ = elimSetQuotientsProp (λ _ → 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ℓℕ)