Every parametric function between functors is natural

NatForFree.agda

-- Agda 2.6.1, stdlib 1.5

open import Relation.Binary.PropositionalEquality
  renaming (sym to infix 6 _⁻¹; cong to ap; trans to infixr 5 _◾_; subst to tr)
open import Function

coe : ∀{i}{A B : Set i} → A ≡ B → A → B
coe refl a = a

Rel : Set → Set → Set₁
Rel A B = A → B → Set

Id : (A : Set) → Rel A A
Id A x y = x ≡ y

Graph : {A B : Set} → (A → B) → Rel A B
Graph f a b = f a ≡ b

happly : ∀{i j}{A : Set i}{B : Set j}{f g : A → B} → f ≡ g → ∀ x → f x ≡ g x
happly refl x = refl

record Functor : Set₁ where
  field
    !      : Set → Set
    map    : {A B : Set} → (A → B) → ! A → ! B
    map-id : ∀ {A} → map {A} id ≡ id
    map-∘  : ∀ {A B C}(f : B → C)(g : A → B) → map (f ∘ g) ≡ map f ∘ map g

record Functorᴿ (F : Functor) : Set₁ where
  private module F = Functor F
  field
    !     : ∀{A₀ A₁} → Rel A₀ A₁ → Rel (F.! A₀) (F.! A₁)
    map   : ∀ {A₀ A₁}(Aᴿ : Rel A₀ A₁){B₀ B₁}(Bᴿ : Rel B₀ B₁)
            (f₀ : A₀ → B₀)(f₁ : A₁ → B₁)(fᴿ : ∀ {a₀ a₁} → Aᴿ a₀ a₁ → Bᴿ (f₀ a₀) (f₁ a₁))
            {fa₀ fa₁} → ! Aᴿ fa₀ fa₁ → ! Bᴿ (F.map f₀ fa₀) (F.map f₁ fa₁)

    idext : ∀ {A} → ! (Id A) ≡ Id (F.! A)

  reflexive : ∀ {A x} → ! (Id A) x x
  reflexive {A} {x} = tr (λ f →  f x x) (idext ⁻¹) refl

module _
  (F G : Functor) (Fᴿ : Functorᴿ F) (Gᴿ : Functorᴿ G) where

  module F  = Functor F   ; module G  = Functor G
  module Fᴿ = Functorᴿ Fᴿ ; module Gᴿ = Functorᴿ Gᴿ

  module _ (η  : ∀ {A} → F.! A → G.! A)
           (ηᴿ : ∀ {A₀ A₁}(Aᴿ : Rel A₀ A₁){fa₀ fa₁}
                 → Fᴿ.! Aᴿ fa₀ fa₁ → Gᴿ.! Aᴿ (η fa₀) (η fa₁)) where

    η-is-natural : ∀ {A B}(f : A → B) x → G.map f (η x) ≡ η (F.map f x)
    η-is-natural {A} {B} f x =
      let lem1 : Fᴿ.! (Graph f) (F.map id x) (F.map f x)
          lem1 = Fᴿ.map (Id A) (Graph f) id f (ap f) {x} {x} Fᴿ.reflexive

          lem2 : Fᴿ.! (Graph f) x (F.map f x)
          lem2 = tr (λ y → Fᴿ.! (Graph f) y (F.map f x)) (happly F.map-id x) lem1

          lem3 : Gᴿ.! (Graph f) (η x) (η (F.map f x))
          lem3 = ηᴿ (Graph f) lem2

          lem4 : Gᴿ.! (Id B) (G.map f (η x)) (G.map id (η (F.map f x)))
          lem4 = Gᴿ.map (Graph f) (Id B) f id id lem3

          lem5 : Gᴿ.! (Id B) (G.map f (η x)) (η (F.map f x))
          lem5 = tr (λ y → Gᴿ.! (Id B) (G.map f (η x)) y) (happly G.map-id _) lem4

      in coe (happly (happly Gᴿ.idext (G.map f (η x))) (η (F.map f x))) lem5