## Stream: new members

### Topic: universes in lean

#### Harsha Nyapathi (Dec 24 2019 at 05:55):

I have tried to represent graphs and paths using inductive data type in lean.
https://github.com/enharsha/Graphs-in-Lean/blob/master/graph.lean
However, while compiling definition of path, it shows the following error - "universe level of type_of(arg #3) of 'path.addedge' is too big for the corresponding inductive datatype". Could anyone help me out? I have referred to inductive types section in Theorem Proving in Lean, where vectors have been defined in a similar fashion.

#### Johan Commelin (Dec 24 2019 at 06:00):

Well, your edges live in some universe v, and paths must live (by your definition) in universe u. That doesn't fit...

#### Johan Commelin (Dec 24 2019 at 06:01):

So, either you just use one universe, or paths should live in Type (max u v)

#### Johan Commelin (Dec 24 2019 at 06:01):

Also, when you write g : graph, I feat that Lean can't figure out the universes by itself. So maybe you need to write g : graph.{u v}

#### Yury G. Kudryashov (Dec 24 2019 at 06:28):

Another approach is to define

universes v u
structure graph (α : Type u) := (edges : α → α → Type v)


This is similar to the approach taken by category_theory.category. Not sure which approach is better.

#### Jesse Michael Han (Dec 24 2019 at 06:41):

this compiles for me:

inductive path (g : graph.{u v}) (start : g.vertex) : (g.vertex) → Type (max u v)
| fix : path start


#### Kevin Buzzard (Dec 24 2019 at 09:57):

I know it's sacreligious to suggest this here but you could just put vertices in edges in the same universe (something mathematicians have been doing for 100 years) and then you can just forget all about them

#### Harsha Nyapathi (Dec 26 2019 at 11:12):

Yes, mismatch of the universes seems to be the issue. It compiles now. Thanks a lot!

#### Yury G. Kudryashov (Dec 27 2019 at 07:15):

@Harsha Nyapathi It seems to me that

universes v u
structure graph (α : Type u) := (edge : α → α → Type v)


requires fewer equality assumptions in various lemmas. E.g., paths can be defined as

inductive path {α : Type u} (g : graph.{v} α) (start : α) : α → Type (max v u)
| fix : path start
| addedge {last : α} (p : path last) {last' : α} (e : g.edge last last') : path last'


Of course, a downside of this approach is that you need to write {v₁ v₂ : α} (e : g.edge v₁ v₂) instead of e : g.edge.
Another bonus of this definition is that it makes easier to define, e.g., the graph corresponding to a category (no need to bundle homs with domain/codomain).

Last updated: May 09 2021 at 19:11 UTC