invalid occurrence of universe level

Stream: mathlib4

[Kevin Buzzard]

I have a universe error which I can't fathom out; this arises when porting Logic.Equiv.Basic.

import Mathlib.Logic.Equiv.Defs
import Mathlib.Data.Prod.Basic

namespace Equiv

def prodCongr {α₁ β₁ α₂ β₂ : Type _} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : α₁ × β₁ ≃ α₂ × β₂ :=
  ⟨Prod.map e₁ e₂, Prod.map e₁.symm e₂.symm, fun ⟨a, b⟩ => by simp, fun ⟨a, b⟩ => by simp⟩
#align equiv.prod_congr Equiv.prodCongr

def prodPUnit (α : Type _) : α × PUnit.{u + 1} ≃ α :=
  ⟨fun p => p.1, fun a => (a, PUnit.unit), fun ⟨_, PUnit.unit⟩ => rfl, fun _ => rfl⟩

def prodUnique (α β : Type _) [Unique β] : α × β ≃ α :=
  ((Equiv.refl α).prodCongr <| equivPUnit β).trans <| prodPUnit α
/-
invalid occurrence of universe level 'u_3' at 'Equiv.prodUnique', it does not occur at the declaration type, nor it is explicit universe level provided by the user, occurring at expression
  Equiv.trans.{max (u_1 + 1) (u_2 + 1), max (u_1 + 1) (u_3 + 1), u_1 + 1}
    (prodCongr.{u_1, u_2, u_1, u_3} (Equiv.refl.{u_1 + 1} α) (equivPUnit.{u_2 + 1, u_3 + 1} β)) (prodPUnit.{u_3, u_1} α)
at declaration body
  fun (α : Type u_1) (β : Type u_2) [Unique β] => Equiv.trans (prodCongr (Equiv.refl α) (equivPUnit β)) (prodPUnit α)
-/

Any clues?

[Gabriel Ebner]

It means that the universe level of the PUnit is unspecified in the body of the definition.

[Gabriel Ebner]

It could be v+1 or v+100 or etc. (if β : Type v)

[Gabriel Ebner]

def prodUnique (α : Type u) (β : Type v) [Unique β] : α × β ≃ α :=
  ((Equiv.refl α).prodCongr <| equivPUnit.{v+1,v+10} β).trans <| prodPUnit α

[Gabriel Ebner]

Not sure where to best put the level annotation.

[Kevin Buzzard]

Thanks! This worked in Lean 3. Is this something which needs flagging?

[Kevin Buzzard]

wooah I went for v + 37 of course, and I got

maximum universe level offset threshold (32) has been reached, you can increase the limit using option `set_option maxUniverseOffset <limit>`, but you are probably misusing universe levels since offsets are usually small natural numbers

[Kevin Buzzard]

lol at "you are probably misusing universe levels"

[Kevin Buzzard]

PS is the name pUnitProd for PUnit × α ≃ α? My understanding is that we're not going for lE but perhaps pUnit is less bad

[Mario Carneiro]

I've been using punitProd when it shows up at the beginning of a word... I guess that's not consistent with the current advice

[Scott Morrison]

I like punit too.

[Arien Malec]

Can someone have a look at PR 649 which typecheck but lints with similar issues?

[Arien Malec]

Sorry PR #638

[Arien Malec]

(On mobile- excuse the bad link)

[Yakov Pechersky]

Related question: why is the second style of epi invalid?

def epi {A B Z : Type _} (f : A → B) : Prop :=
    ∀ ⦃g g' : B → Z⦄, g ∘ f = g' ∘ f → g = g'

def epi' {A B : Type _} (f : A → B) : Prop :=
    ∀ {Z : Type _} ⦃g g' : B → Z⦄ (h : g ∘ f = g' ∘ f), g = g'
/-
invalid occurrence of universe level 'u_3' at 'epi'', it does not occur at the declaration type, nor it is explicit universe level provided by the user, occurring at expression
  ∀ {Z : Type u_3} ⦃g g' : B → Z⦄,
    Eq.{max (u_1 + 1) (u_3 + 1)} (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} g f)
        (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} g' f) →
      Eq.{max (u_2 + 1) (u_3 + 1)} g g'
at declaration body
  fun {A : Type u_1} {B : Type u_2} (f : A → B) => ∀ {Z : Type u_3} ⦃g g' : B → Z⦄, g ∘ f = g' ∘ f → g = g'
-/

[Kevin Buzzard]

Does anything change if you make all universes explicit?

[Yakov Pechersky]

Yes, that's better, thanks!

set_option autoImplicit false

universe u v w

def epi {A B Z : Sort _} (f : A → B) : Prop :=
    ∀ ⦃g g' : B → Z⦄, g ∘ f = g' ∘ f → g = g'

def epi' {A : Sort u} {B : Sort v} (f : A → B) : Prop :=
    ∀ {Z : Sort w} ⦃g g' : B → Z⦄, g ∘ f = g' ∘ f → g = g'

def Surjective {α β : Sort _} (f : α → β) : Prop := ∀ b, ∃ a, f a = b

example {A B : Sort _} (f : A → B) :
    Surjective f ↔ ∀ Z, epi (Z := Z) f := by
  constructor
  · intro h Z g g' hg
    funext b
    cases h b with
    | intro a ha =>
      rw [←ha]
      exact congrFun hg a
  · intro h b
    specialize @h Prop (λ x => ∃ a, f a = x) (λ _ => True) _
    · funext a
      exact eq_true ⟨a, rfl⟩
    · simp [congrFun h b]

example {A B : Sort _} (f : A → B) :
    Surjective f ↔ epi' f := by
  constructor
  · intro h Z g g' hg
    funext b
    cases h b with
    | intro a ha =>
      rw [←ha]
      exact congrFun hg a
  · intro h b
    specialize @h Prop (λ x => ∃ a, f a = x) (λ _ => True) _
    · funext a
      exact eq_true ⟨a, rfl⟩
    · simp [congrFun h b]

[Kevin Buzzard]

Is this expected behaviour or a bug? I'm surprised by it.

[Sophie Morel]

Kevin Buzzard said:

I have a universe error which I can't fathom out; this arises when porting Logic.Equiv.Basic.
<snip>

I am having a similar problem while trying to port Shing Tak Lam's formalization of abstract simplicial complexes from Lean3 to Lean4. I am also not sure how to adapt Gabriel's solution to my case, I tried sticking universes everywhere but, well, I'm not that good with Lean4 and I just get more errors. I'm getting really sleepy now, so I'll try some more tomorrow and maybe extract a MWE if nothing works.

[Kevin Buzzard]

Universes are a bit of a dark art in Lean 4; I guess the community are slowly learning how to tame them. Is your port part of the official porting effort? If so you could post a link to the PR.

[Sophie Morel]

No, it's part of my translating my personal project into Lean4., though I do hope that abstract simplicial complexes eventually are integrated into mathlib4. (I started learning Lean4 about a week ago, so I'm not sure I should be trusted anywhere near the official porting effort.)

[Sophie Morel]

Okay, I think one of my problems is coming from the fact that I define a Bot instance using the empty set, but Lean doesn't know which universe this empty set lives in. How do I tell it "you know, I mean the smallest element of (Set (Finset α)), it's definitely still in the same universe u" ? I've been embarrassingly stuck on this particular point for like 30 minutes. :sad:
Uh, never mind, it was ∅ : Set (Finset V) of course.

[Sophie Morel]

Okay, the problem seems to have gone away but I have no idea why... I was trying to put a CompleteLattice instance on the type of abstract simplicial complex on a type V (defined as a set of finsets of V with some properties), I had already defined Bot and Top instances, Lean was complaining that there was some universe problem to do with them. So I defined OrderBot and OrderTop instances separately with explicit universe declarations, used them in the definition of the CompleteLattice instance (instead of just using Bot and Top plus proofs of bot_le and le_top), and suddenly Lean is happy ? :astonished:

[Sophie Morel]

Tune back in for the next 5 minutes, when I will try to make the CompleteLattice`` into a CompleteDistribLattice``` and the problem will come back with a vengeance...

[Reid Barton]

Whether or not the epi/epi' behavior was intended, it definitely seems good to me--it's very rare that you want to make a declaration like epi', and if you do you should be explicit about what you're doing.

[Reid Barton]

A priori the propositions epi'.{u v w} f are all different for different w--in this case we know they actually are equal. Though I'm pretty sure your example only proves this for epi'.{u v 0} f. Note you can't even see this by looking at the statement, you have to look at the proof!

[Yaël Dillies]

@Sophie Morel, if you give us a #mwe we can have a go at debugging.

[Sophie Morel]

@Yaël Dillies Thanks, but I solved the problem by myself. I'm still not sure what happened, but Lean is happy, so I am happy.

[Sophie Morel]

(In fact it was while trying to produce a MWE short enough for Zulip that I accidentally solved the problem.)

[Patrick Massot]

This is actually one of the reasons why we ask for MWE. Note this also happen with real life math conversations.

[Yakov Pechersky]

@Reid, how would you formalize this exercise?
image.png
image.png

[Yakov Pechersky]

BTW, switching from example to theorem breaks the proofs

[Reid Barton]

Just use one universe for everything

[Yakov Pechersky]

So one has to specify universes more explicitly, and yes, the proofs end up in Sort 1:

set_option autoImplicit false
set_option pp.universes true

universe u v w

def epi {A : Sort u} {B : Sort v} {Z : Sort w} (f : A → B) : Prop :=
    ∀ ⦃g g' : B → Z⦄, g ∘ f = g' ∘ f → g = g'

def epi' {A : Sort u} {B : Sort v} (f : A → B) : Prop :=
    ∀ {Z : Sort w} ⦃g g' : B → Z⦄, g ∘ f = g' ∘ f → g = g'

def Surjective {α β : Sort _} (f : α → β) : Prop := ∀ b, ∃ a, f a = b

theorem foo {A B : Sort _} (f : A → B) :
    Surjective f ↔ ∀ Z, epi.{u, v, 1} (Z := Z) f := by
  constructor
  · intro h Z g g' hg
    funext b
    cases h b with
    | intro a ha =>
      rw [←ha]
      exact congrFun hg a
  · intro h b
    specialize @h Prop (λ x => ∃ a, f a = x) (λ _ => True) _
    · funext a
      exact eq_true ⟨a, rfl⟩
    · simp [congrFun h b]

theorem bar {A : Sort u} {B : Sort v} (f : A → B) :
    Surjective f ↔ epi'.{u, v, 1} f := by
  constructor
  · intro h Z g g' hg
    funext b
    cases h b with
    | intro a ha =>
      rw [←ha]
      exact congrFun hg a
  · intro h b
    specialize @h Prop (λ x => ∃ a, f a = x) (λ _ => True) _
    · funext a
      exact eq_true ⟨a, rfl⟩
    · simp [congrFun h b]

[Reid Barton]

That's what the author of those texts meant anyways

[Yakov Pechersky]

Yes, I guess so:

theorem foo {A B : Type} (f : A → B) :
    Surjective f ↔ ∀ Z, epi (Z := Z) f := by
  constructor
  · intro h Z g g' hg
    funext b
    cases h b with
    | intro a ha =>
      rw [←ha]
      exact congrFun hg a
  · intro h b
    specialize @h Prop (λ x => ∃ a, f a = x) (λ _ => True) _
    · funext a
      exact eq_true ⟨a, rfl⟩
    · simp [congrFun h b]

theorem bar {A B : Type} (f : A → B) :
    Surjective f ↔ epi' f := by
  constructor
  · intro h Z g g' hg
    funext b
    cases h b with
    | intro a ha =>
      rw [←ha]
      exact congrFun hg a
  · intro h b
    specialize @h Prop (λ x => ∃ a, f a = x) (λ _ => True) _
    · funext a
      exact eq_true ⟨a, rfl⟩
    · simp [congrFun h b]

[Yakov Pechersky]

What would be the proof in other universes? With ulift Prop?

[Reid Barton]

You can also make your theorem bar work for any w, by using ULift Prop, and some extra messing about. (Okay, maybe not w = 0, didn't think about it.)

[Reid Barton]

(There are also other constructions that work, e.g., take Z to be the quotient of two copies of B by the relation that identifies the two copies of f(a) for each a in A)

[Reid Barton]

If this was a general notion of epimorphism in a category being specialized to the category of types, then you would be forced to put A, B, Z all in a single universe anyways.

[Reid Barton]

But the main point I think is that your epi' does not say that "for all sets $Z$ and ...". Rather, there is a whole family of different epi'.{u,v,w} which say that "for all w-small sets $Z$ and ...", i.e., you've defined what it means for f to be a w-epimorphism for each w, where w is some universe variable that is totally independent of f.

[Reid Barton]

In this case the meanings of those statements seem to be

• Every map f is a 0-epimorphism (because any two maps into a propositions are equal), while
• a map f is w+1-epimorphism if and only if it is an epimorphism in the usual sense

[Reid Barton]

I think we can assume that this is not what the author of those texts had in mind.

[Reid Barton]

I'm not saying it is a useless thing or that you don't want to do it, just that probably it should not be as easy to do accidentally as writing a Type _ on autopilot.

[Yakov Pechersky]

Thanks for that detailed explanation

[Yakov Pechersky]

So, having one universe for A B Z, and probably just doing Type is good enough. For posterity, this is what I now have, just experimentation that does compile:

set_option autoImplicit false
-- set_option pp.universes true

universe u

def epi {A : Sort u} {B : Sort u} {Z : Sort u} (f : A → B) : Prop :=
    ∀ ⦃g g' : B → Z⦄, g ∘ f = g' ∘ f → g = g'

def epi' {A : Sort u} {B : Sort u} (f : A → B) : Prop :=
    ∀ {Z : Sort u} ⦃g g' : B → Z⦄, g ∘ f = g' ∘ f → g = g'

def Surjective {α β : Sort _} (f : α → β) : Prop := ∀ b, ∃ a, f a = b

theorem foo {A B : Type u} (f : A → B) :
    Surjective f ↔ ∀ (Z : Type u), epi (Z := Z) f := by
  constructor
  · intro h Z g g' hg
    funext b
    cases h b with
    | intro a ha =>
      rw [←ha]
      exact congrFun hg a
  · intro h b
    specialize @h (ULift Prop) (λ x => ULift.up $ ∃ a, (f a = x)) (λ _ => ULift.up True) _
    · funext a
      simp [eq_true (⟨a, rfl⟩ : ∃ x, f x = f a)]
    · have := congrArg ULift.down (congrFun h b)
      rw [ULift.down_up, ULift.down_up] at this
      simp [this]

theorem bar {A B : Type u} (f : A → B) :
    Surjective f ↔ epi' f := by
  constructor
  · intro h Z g g' hg
    funext b
    cases h b with
    | intro a ha =>
      rw [←ha]
      exact congrFun hg a
  · intro h b
    specialize @h (ULift Prop) (λ x => ULift.up $ ∃ a, (f a = x)) (λ _ => ULift.up True) _
    · funext a
      simp [eq_true (⟨a, rfl⟩ : ∃ x, f x = f a)]
    · have := congrArg ULift.down (congrFun h b)
      rw [ULift.down_up, ULift.down_up] at this
      simp [this]

[Reid Barton]

Probably what you'd really like to write is epi'' f := "for all universes w and Z : Type w, and ..." but Lean doesn't allow this.