Zulip Chat Archive

Stream: general

Topic: HoTT3 universe errors


Thomas Eckl (Aug 29 2020 at 12:14):

I started to port my Lean2 - HoTT files to HoTT3, but run almost immediately into trouble:

import hott.init

universes u v w
hott_theory

namespace hott

@[hott, hsimp, reducible]
def id {A : Type u} (a : A) : A := a

@[hott, hsimp, reducible]
def id_map (A : Set) : A -> A := @id A

@[hott]
lemma id_map_is_right_neutral {A B : Set} (map : A -> B) :
  map  (id_map A) = map :=
by { hsimp, exact rfl }

end hott

says goals accomplished at the last } but attaches a problem to the equality sign in id_map_is_right_neutral:

kernel failed to type check declaration 'id_map_is_right_neutral' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  Π {A : Set} {B : Set} (map : A  B), map  id_map A = map
elaborated value:
  λ {A : Set} {B : Set} (map : A  B), cast idp⁻¹ rfl
nested exception message:
type mismatch at application
  @eq (A  B)
term
  A  B
has type
  Type (max u_1 u_2)
but is expected to have type
  Type u_3

I never understand these universe error messages. Why is ↥A → ↥B expected to have type Type u_3? Why can't u_3 be unified with max u_1 u_2? You get more or less the same message when replacing exact rfl by exact @hott.eq.refl (A -> B) map. I also wonder why you can't use reflexivity for hott.eq.

Thomas Eckl (Aug 29 2020 at 12:17):

I also have some fundamental questions about the implementation of HoTT in Lean 3: Why can't you just check whether terms use objects of type Prop in their construction? Isn't that the only way how HoTT and Lean 3 can produce contradiction?

Gabriel Ebner (Aug 29 2020 at 13:32):

The error happens, as the error message explains, because the tactic is probably buggy (because it generates an incorrect proof term). But I don't have time to debug that right now. Feel free to file an issue though.

Gabriel Ebner (Aug 29 2020 at 13:33):

You can definitely use reflexivity for hott.eq, we use it all over the place. If it doesn't work here, then that might be related to same issue as above.

Gabriel Ebner (Aug 29 2020 at 13:36):

Why can't you just check whether terms use objects of type Prop in their construction?

That is, very generally speaking, exactly what the @[hott] attribute does. It is a bit more permissive though, it allows everything except eq.rec, acc.rec, heq.rec and choice (those are the only recursors/axioms that produce something outside of Prop).

Thomas Eckl (Aug 29 2020 at 19:48):

My guess would be the bug in the builtin elaborator, because the issue remains when you replace by ... with sorry. Is it then a Lean 3 problem?

Floris van Doorn (Aug 29 2020 at 23:09):

This is strange. I have minimized the problem, and here is a code snippet that fails in the latest version of Lean, without using anything HoTT-specific:

-- set_option trace.elaborator_detail true

def my_eq {A : Type*} (a b : A) : Prop := true

lemma id_map_is_right_neutral {A : Type} (map : A -> A) :
  my_eq (function.comp.{1 1 _} map map) map :=
sorry

Kevin Buzzard (Aug 29 2020 at 23:13):

Does changing Type* to Type u help?

Floris van Doorn (Aug 29 2020 at 23:25):

no (changing it to Type/Sort*/Sort u does)

Floris van Doorn (Aug 29 2020 at 23:27):

It is strange that @Thomas Eckl runs into this problem, but apparently it wasn't a problem for the rest of the HoTT library.

Kevin Buzzard (Aug 29 2020 at 23:28):

universe u

def my_eq {A : Type u} (a b : A) : Prop := true

lemma id_map_is_right_neutral {A : Type} (maap : A -> A) :
  my_eq (function.comp maap maap) maap := trivial

->

kernel failed to type check declaration 'id_map_is_right_neutral' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  ∀ {A : Type} (maap : A → A), my_eq (maap ∘ maap) maap
elaborated value:
  λ {A : Type} (maap : A → A), trivial
nested exception message:
type mismatch at application
  @my_eq (A → A)
term
  A → A
has type
  Type
but is expected to have type
  Type u_1

Interesting!

Thomas Eckl (Sep 01 2020 at 16:51):

I've got the same error message when stating the universal property of injective maps (of sets):

@[hott]
lemma univ_prop_of_inj {A B : Set} (i : A -> B) (i_inj : is_set_injective i) :
  forall (C : Set) (f g : C -> A), i  f = i  g -> f = g :=
sorry

I hope is_set_injective is self-explaining, but you can produce the error message also by omitting the parameteri_inj.
The scientist in me immediately induces from these two observations that the problem might be related to the composition of functions. Hovering over the shows that composition is taken from the general Lean3 library (init.function), not from HoTT3. And in Lean3, all the domains and codomains of the maps are sorts, not types - maybe that clashes with = of maps between types?

Since I did not find a definition of in hott.init.function, I guess it does not exist anywhere. Should it be added to hott.init.function?

Thomas Eckl (Sep 01 2020 at 17:07):

Just tried: Inserting in my file

namespace function

@[inline, reducible] def comp {α β φ : Type _} (f : β  φ) (g : α  β) : α  φ :=
λ x, f (g x)

infixr  ` ∘ʰ `:80      := hott.function.comp

end function

solves the problem. The new symbol is not perfect, but also not too bad ...

Floris van Doorn (Sep 01 2020 at 17:09):

Yes, it has to do with the interaction of Sort and Type between hott.eq and function.comp. I don't know why though, I feel like Lean should be able to figure it out. Moreover, Lean managed to figure out all the occurrences of composition in init.

Floris van Doorn (Sep 01 2020 at 17:10):

If in the hott namespace you write

def function.comp {A B C : Type _} (g : B  C) (f : A  B) (x : A) := g (f x)
hott_theory_cmd "local infix ` ∘ ` := hott.function.comp"

then you override the notation to mean hott.function.comp (so you can use the same symbol)


Last updated: Dec 20 2023 at 11:08 UTC