HoTT3 universe errors

Stream: general

[Thomas Eckl]

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]

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]

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]

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]

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]

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]

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]

Does changing Type* to Type u help?

[Floris van Doorn]

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

[Floris van Doorn]

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]

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]

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]

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]

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]

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)