Fix

Scratch.agda

module Scratch where

open import Level
open import Function
open import Relation.Binary.PropositionalEquality
import Relation.Binary.EqReasoning as EqReasoning

-- Legend has it that parametricity is just dinaturality
module Parametricity {a} {F G : Set a → Set a → Set a}
                         (mapF : ∀ {A B C D} → (A → B) → (C → D) → F B C → F A D)
                         (mapG : ∀ {A B C D} → (A → B) → (C → D) → G B C → G A D)
                         where
  postulate
    -- Agda doesn't know that its own polymorphic functions are dinatural, so we must teach it about itself
    dinatural : ∀ (f : ∀ {A} → F A A → G A A) {A B : Set a} (g : A → B) → ∀ x → mapG id g (f (mapF g id x)) ≡ mapG g id (f (mapF id g x))

open Parametricity {zero} {λ A B → A → B} {λ _ A → A} (λ f g h → g ∘ h ∘ f) (λ _ f → f)

definition : (fix : {A : Set} → (A → A) → A) {A : Set} (g : A → A) → fix g ≡ g (fix g)
definition fix g = sym (dinatural fix g id)