fix universe levels for coherentIso

Stream: Infinity-Cosmos

[Emily Riehl]

@Mario Carneiro likes to make fun of me for being bad at universe levels in Lean. Anyway I need some help fixing a universe issue created by the merge of @Arnoud van der Leer's recent PR.

This involved defining

/-- This is the free-living isomorphism as a category with objects called
`zero` and `one`. Perhaps these should have different names?-/
def WalkingIso : Type := Fin 2

then

/-- The simplicial set that encodes a single isomorphism. Its n-simplices are sequences of arrows in WalkingIso. -/
def coherentIso : SSet := nerve WalkingIso

The problem is that this means coherentIso is a simplicial set at universe level 0 (which of course it is). But if we use it as the interval object I in various constructions, it forces the simplicial sets to also be at universe level 0.

/-- TODO: Figure out how to allow `I` to be an a different universe from `A` and `B`?-/
structure Homotopy {A B : SSet.{u}} (f g : A ⟶ B) : Type u
    where
  homotopy : A ⟶ sHom I B
  source_eq : homotopy ≫ pathSpace.src B = f
  target_eq : homotopy ≫ pathSpace.tgt B = g

/-- For the correct interval, this defines a good notion of equivalences for both Kan complexes and quasi-categories.-/
structure Equiv (A B : SSet.{u}) : Type u where
  toFun : A ⟶ B
  invFun : B ⟶ A
  left_inv : Homotopy (I := I) (toFun ≫ invFun) (𝟙 A)
  right_inv : Homotopy (I := I) (invFun ≫ toFun) (𝟙 B)

How do I fix this? At the moment there are also universal level errors in the InfinityCosmos.Basic file which I'm hoping is caused by this, but I'm not sure.

[Joël Riou]

Using ULift.{u} (Fin 2) should make coherentIso a universe polymorphic definition.

[Arnoud van der Leer]

To prevent this in the future, is there an introduction to (our) usage of universe levels in Lean? Some reading material?

[Emily Riehl]

I needed also to add some ULift.ups:

def WalkingIso : Type u := ULift (Fin 2)

def WalkingIso.zero : WalkingIso := ULift.up (0 : Fin 2)
def WalkingIso.one : WalkingIso := ULift.up (1 : Fin 2)

[Emily Riehl]

which then proliferate:

/-- From an isomorphism in a category, one can build a functor out of `WalkingIso` to
that category.-/
def fromIso {X Y : C} (e : X ≅ Y) : WalkingIso ⥤ C where
  obj := fun
    | ULift.up (0 : Fin 2) => X
    | ULift.up (1 : Fin 2) => Y
  map := @fun
    | ULift.up (0 : Fin 2), ULift.up (0 : Fin 2), _ => 𝟙 _
    | ULift.up (0 : Fin 2), ULift.up (1 : Fin 2),  _ => e.hom
    | ULift.up (1 : Fin 2), ULift.up (0 : Fin 2), _ => e.inv
    | ULift.up (1 : Fin 2), ULift.up (1 : Fin 2),  _ => 𝟙 _
  map_comp := by simp [WalkingIso, Quiver.Hom]

[Aaron Liu]

you can @[match_pattern] on WalkingIso.zero and WalkingIso.one

[Emily Riehl]

This makes me think we might not have the right API set up. Previously this was defined as an inductive type with two constructors.

inductive WalkingIso : Type u where
  | zero : WalkingIso
  | one : WalkingIso

Which approach is better?

[Mario Carneiro]

it's stylistic, but I prefer the inductive type

[Emily Riehl]

If I understand correctly

@[match_pattern]
def WalkingIso.zero : WalkingIso := ULift.up (0 : Fin 2)

@[match_pattern]
def WalkingIso.one : WalkingIso := ULift.up (1 : Fin 2)

effectively restores the inductive type?

[Aaron Liu]

it lets you do match x with | WalkingIso.zero => ... | WalkingIso.one => ...

[Emily Riehl]

Now I have an issue where I'm trying to define an equivalence between X -> ULift.u Y and X -> Y, where the arrow is just function types.

[Emily Riehl]

I think I got it:

/-- Since the morphisms in WalkingIso do not carry information, an n-simplex of coherentIso is equivalent to an (n + 1)-vector of the objects of WalkingIso. -/
def equivFun {n : ℕ} : coherentIso _⦋n⦌ ≃ (Fin (n + 1) → Fin 2) where
  toFun f := ULift.down ∘ f.obj
  invFun f := .mk (ULift.up ∘ f) (fun _ ↦ ⟨⟩) (fun _ ↦ rfl) (fun _ _ ↦ rfl)
  left_inv _ := rfl
  right_inv _ := rfl

[Eric Wieser]

Another option would be

structure  WalkingIso : Type u where
  ofFin :: toFin : Fin 2

def WalkingIso.zero : WalkingIso := .ofFin (0 : Fin 2)
def WalkingIso.one : WalkingIso := .ofFin (1 : Fin 2)

[Eric Wieser]

Which is maybe less ugly than using up and down

[Emily Riehl]

Could you remind me what the syntax :: means in Lean? I've seen it before but I've forgotten.

I tried experimenting with this definition but it broke a few other things that I wasn't sure how to fix. But anyway I've finally got a non-broken repo after updating some of @Julian Komaromy's to use the mathlib versions of Edge and CompStruc :sweat_smile:

[Mario Carneiro]

that's list cons

[Emily Riehl]

Mario Carneiro said:

that's list cons

What's that in math speak?

[Mario Carneiro]

$a_0 :: [a_1,\dots,a_n] = [a_0,\dots,a_n]$

[Emily Riehl]

Here WalkingIso is a structure with one field, which is a term of type Fin 2. But how should I interpret the ofFin :: toFin?

[Mario Carneiro]

oh that's a different ::

[Mario Carneiro]

structure Foo where mkFoo ::
  a : Nat
  b : Nat

here mkFoo :: is naming the constructor, which is named mk by default

[Mario Carneiro]

it's also used if you want to hang some docs on the constructor

[Emily Riehl]

I see. So toFin is the destructor and ofFin is the constructor?

[Mario Carneiro]

yes

[Mario Carneiro]

I assume the full definition has structure Fin where or the like immediately before it

[Emily Riehl]

I think the summary of this discussion is maybe we should PR some of the basic stuff around WalkingIso and coherentIso to mathlib and see what the pros think is most efficient. @Arnoud van der Leer do you have any interest in attempting this?

[Kevin Buzzard]

One of my favourite definitions in Lean is

structure ULift.{r, s} (α : Type s) : Type (max s r) where
  /-- Wraps a value to increase its type's universe level. -/
  up ::
  /-- Extracts a wrapped value from a universe-lifted type. -/
  down : α

which creates ULift and also

ULift.up.{r, s} {α : Type s} (down : α) : ULift α

and

ULift.down.{r, s} {α : Type s} (self : ULift α) : α

In Lean 3 it was just

structure {r s} ulift (α : Type s) : Type (max s r) :=
up :: (down : α)

[Emily Riehl]

@Kevin Buzzard it's hilarious to me that this is one of your favorite definitions...

Whenever ULift comes up I get a headache and start to lose faith about formalization as the future of mathematical proof writing...

I'm teaching category theory this semester and one of the things I'm agonizing over is whether to try to be a bit more precise about universe levels. It would feel more honest if somehow I were (since in category theory it actually matters in the sense that if you get it wrong the theorem might be false) but it's just too much. Today, for instance, I defined functor categories en route to discussing the 2-category of categories. I did mention briefly that this is one of the constructions that might increase sizes but didn't go into details. The rest of the lecture was one proofs by diagram chases, applied, eg, to prove that the horizontal and vertical composites of two natural transformations are natural.

[Kevin Buzzard]

I just thought it was a beautiful definition! I saw it just as I was beginning to learn something about functional programming. I'm well aware that it's causing you problems :-(

[Arnoud van der Leer]

Emily Riehl said:

I think the summary of this discussion is maybe we should PR some of the basic stuff around WalkingIso and coherentIso to mathlib and see what the pros think is most efficient. Arnoud van der Leer do you have any interest in attempting this?

I could give it a try in the coming weeks.
What would it entail? Is there a guide to this, somewhere?

[Emily Riehl]

Here's the guide.

If you'd like to have a zoom chat, let me know. Alternatively, please tag me when the PR is up and I'll have a look at the code.

[Arnoud van der Leer]

Thanks! Just to get this straight:
In our case, we are working in a repository that uses mathlib as a package. So then PRing this to mathlib means forking mathlib, adding my additions to that fork and PRing that. (And at some point remove the additions from our forMathlib folder again).
Right?

[Kevin Buzzard]

I think people usually say "uses mathlib as a dependency" but what you're describing is exactly how we run FLT; you remove the additions once the PR is merged and your repo is bumped to include the merged mathlib commits.

[Arnoud van der Leer]

I submitted it in #35287