Zulip Chat Archive

Stream: general

Topic: automorphisms of the universe


view this post on Zulip Johan Commelin (Jan 16 2020 at 14:09):

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

view this post on Zulip Chris Hughes (Jan 16 2020 at 14:13):

It can't be done constructively though.

view this post on Zulip Johan Commelin (Jan 16 2020 at 14:14):

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


Last updated: May 14 2021 at 00:42 UTC