## 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: May 18 2021 at 17:44 UTC