HoTT question

Stream: general

[Kevin Buzzard]

I've been chatting to Martin Escudo, someone who knows a lot more about univalence than me. My understanding of one of his claims was that it was impossible to define (in Lean) a predicate P on types such that P(nat) was provably true and P(int) was provably false. His argument seemed to be that a sufficiently large part of univalence was consistent with Lean. However he said that for functions from Type to Type one could find such functions P in the presence of global choice. My understanding of his claim is that he's saying the following is provable in Lean:

import data.equiv.basic

example (c : ∀ (X : Type), (nonempty X) → X) (P : Type → Type)
  (X Y: Type) (h : P X) (e : X ≃ Y) : P(Y) → false := sorry

In words: in the presence of what he calls "global choice" (c) one can find P : Type -> Type such that P(X) is inhabited but P(Y) isn't, for some isomorphic X and Y. Have I understood him correctly?

[Mario Carneiro]

Your formal statement is certainly false, since you are claiming that this property holds of all P

[Mario Carneiro]

I don't think the claim you attribute to Martin is true either though; even in the presence of global choice it's still possible that nat and int are literally different names for the same underlying type

[Mario Carneiro]

it was impossible to define (in Lean) a predicate P on types such that P(nat) was provably true and P(int) was provably false

I agree with this

However he said that for functions from Type to Type one could find such functions P in the presence of global choice.

I disagree with this unless "find" is meant in a sense other than "there is a definable lean term P such that P(X) is provably true and P(Y) is provably false and X ~= Y is provable"

[Kevin Buzzard]

Aren't I claiming that if univalence holds for all P then we have a contradiction?

[Kevin Buzzard]

Of course anything Martin said about univalence could well have been mangled as it passed through my brain

[Kevin Buzzard]

Oh I have made an elementary error, hang on

[Kevin Buzzard]

import data.equiv.basic

example (c : ∀ (X : Type), (nonempty X) → X)
(h : ∀ (P : Type → Type) (X Y: Type), P X → X ≃ Y → P(Y)) : false := sorry

This is what I meant to claim that he was saying should be provable. Sorry.

[Kevin Buzzard]

"global choice is inconsistent with univalence"

[Mario Carneiro]

That's also false

[Mario Carneiro]

It's not the same as "global choice is inconsistent with univalence" which is true

[Mario Carneiro]

The key data point is that "weak univalence", or A ~= B -> A = B, is consistent with lean

[Mario Carneiro]

which implies that your example statement is not provable

[Mario Carneiro]

example (weak_ua: ∀ {X Y}, X ≃ Y → X = Y) :
  ∀ (P : Type → Type) (X Y: Type), P X → X ≃ Y → P(Y) :=
λ P X Y hX e, eq.mp (congr_arg _ (weak_ua e)) hX

[Mario Carneiro]

Here is a proof that full univalence is false (using proof irrelevance, not choice)

def transport {X Y} : X = Y → X ≃ Y := λ h, eq.rec (equiv.refl _) h
constant ua {X Y} : X ≃ Y → X = Y
axiom ua_left_inv {X Y} (e : X ≃ Y) : transport (ua e) = e

def bswap : bool ≃ bool := ⟨bnot, bnot, bnot_bnot, bnot_bnot⟩

example : false :=
begin
  have h1 : transport (ua bswap) tt = ff :=
    (congr_arg (λ e : bool ≃ bool, e tt) (ua_left_inv bswap):_),
  have h2 : transport (ua bswap) tt = tt :=
    (congr_arg (λ e : bool ≃ bool, e tt) (ua_left_inv (equiv.refl _)):_),
  exact bool.ff_ne_tt (h1.symm.trans h2)
end

[Kevin Buzzard]

Thanks!

[Kevin Buzzard]

That was written just as I went to bed but I now realise that it's just the standard bool thing again. Aut(bool) is not a subsingleton, which is problematic with an impredicative =. But what I'm trying to understand is why global choice contradicts univalence.

[Chris Hughes]

I think it's more or less because if I choose from a non subsingleton type, that choice won't be preserved under a non identity permutation of that type.

[Chris Hughes]

I had a go in HoTT Lean. There are a couple of sorries. Not sure if this is the right idea. Also HoTT Lean wants me to give explicit motives for every substitution. Thinking about it more, I'm not sure if hb' is provable.

@[hott] def bool_not : equiv bool bool :=
equiv.mk bnot $ is_equiv.mk _ bnot
  (λ b, bool.rec_on b rfl rfl) (λ b, bool.rec_on b rfl rfl)
    (λ b, bool.rec_on b rfl rfl)

axiom choice : Π {α : Sort*}, trunc 0 α → α

noncomputable example : empty :=
let b := choice (trunc.tr tt) in
let e : bool = bool := ua bool_not in
let b' : bool := eq.cast e b in
have hb' : b' = choice (trunc.tr ff), from sorry,
have h : b' = bnot b, from cast_ua bool_not b,
have h' : b' = b, from @eq.rec_on _
  (choice (trunc.tr ff)) (λ c _, b' = c) _
    (@eq.rec_on _ (choice (trunc.tr tt)) (λ c _, c = b) _
      (@eq.rec_on _ (trunc.tr ff) (λ c _, choice c = choice (trunc.tr ff)) _
        sorry
        rfl)
      rfl)
    hb',

[Kevin Buzzard]

Martin says that I need to use "full univalence", as other people have pointed out, and because full univalence is just inconsistent with Lean, it's inconsistent with global choice in Lean, as Mario pointed out. I don't think I have a question any more. Thanks Mario and Chris.

[Floris van Doorn]

There are two separate claims here, both of which are true:

• Univalence is inconsistent with proof irrelevance;
• Univalence is inconsistent with global choice.

[Junyan Xu]

I am able to formalize the proof in Lemma 3.8.5 in the HoTT book; the middle paragraph isn't used.

import hott.hit.trunc
open hott
hott_theory

axiom choice : Π {α : Sort*}, trunc -1 α → α

@[hott] example : empty :=
begin
  let X := {A | trunc -1 (bool = A)},
  let x₀ : X := ⟨bool, trunc.tr rfl⟩,
  let : is_contr X,
  { refine ⟨⟨x₀, λ x, _⟩⟩, cases x with x p,
    refine choice (trunc.trunc_functor -1 (λ h, _) p),
    exact sigma.subtype_eq h },
  let hp : is_prop (x₀ = x₀), { resetI, apply_instance },
  let he : (x₀ = x₀) ≃ (bool = bool) := sigma.subtype_eq_equiv x₀ x₀,
  exact bool.not_is_prop_bool_eq_bool (is_trunc.is_trunc_equiv_closed _ he hp),
end

Choice is stated as trunc -1 α → α as it normally is, not trunc 0 α → α. I don't know why @Chris Hughes uses trunc 0 and I don't know whether that version is consistent with univalence.

[Filippo A. E. Nuccio]

Are you sure that with your conventions trunc -1 α → α is in Prop?

[Junyan Xu]

I don't think trunc -1 α → α is in Prop, but trunc -1 α is (more precisely, the type trunc -1 α together with a proof that it is_prop, is a term of type Prop). I think trunc -1 is the HoTT analogue of docs#nonempty, so axiom choice above is the analogue of global choice (docs#classical.choice). trunc 0 α on the other hand truncates α to a set.