Lawvere's theorem

Lawvere.agda

module Lawvere where

open import Function.Equality hiding (cong)
open import Function.Surjection
open import Data.Product
open import Relation.Binary.PropositionalEquality

lawvere : {A B : Set} (f : A ↠ (A → B)) (g : B → B) → ∃ λ x → x ≡ g x
lawvere {A} {B} f g = h a , subst (λ r → h a ≡ g r) (cong (λ f → f a) (from-to refl)) refl
  where
  open Surjection f

  h : A → B
  h x = g ((to ⟨$⟩ x) x)

  a : A
  a = from ⟨$⟩ h