automorphisms of the universe

Stream: general

[Johan Commelin]

Golfing challenge. See also https://mathoverflow.net/questions/350553/is-prod-x-mathcalu-x-to-x-cong-1-admissible-in-type-theory

import tactic

noncomputable theory
open_locale classical

def foo : Π (X : Type), X → X :=
λ X, if h : X = ℕ then by {subst h; exact nat.succ } else id

example (claim : (Π X : Type, X → X) ≃ unit) : false :=
begin
  let bar : Π X : Type, X → X := λ X, id,
  have oops : foo = bar,
  { apply claim.injective,
    apply subsingleton.elim },
  have oops_nat_zero : foo ℕ 0 = bar ℕ 0, by rw oops,
  simp [foo, bar] at *,
  contradiction
end

[Chris Hughes]

It can't be done constructively though.

[Johan Commelin]

Yup, that's what I'm trying to celebrate (-;