stuck at solving universe constraint

Stream: new members

[Shanghe Chen]

Hi the following exercise in category theory:

import Mathlib.CategoryTheory.Types
import Mathlib.CategoryTheory.Yoneda
import Mathlib.CategoryTheory.Limits.Shapes.Pullbacks
import Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
import Mathlib.CategoryTheory.Limits.Shapes.Diagonal
import Mathlib.CategoryTheory.Limits.Types
import Mathlib.CategoryTheory.Limits.Yoneda
import Mathlib.CategoryTheory.Limits.Presheaf

set_option pp.universes true
set_option autoImplicit false

noncomputable section
universe u


open CategoryTheory
open Category
open Limits

variable (C: Type (u+1)) [LargeCategory C] [HasFiniteLimits C]
variable {Y Z : C}
variable (g: Y ⟶ Z)

#check yoneda.obj (pullback.diagonalObj g)
#check (Y ⟶ Z) -- : Type u
#check (yoneda.obj Y ⟶ yoneda.obj Z)  -- : Type (u+1)
#check yoneda.map g

-- set_option trace.Meta.synthInstance true in
-- #synth (HasFiniteLimits (Cᵒᵖ ⥤ Type u))

#check (inferInstance : Category (Cᵒᵖ ⥤ Type u))
#check (pullback.diagonal (yoneda.map g))

gives an error like:

stuck at solving universe constraint
  u =?= max u ?u.10680
while trying to unify
  UnivLE.{max u ?u.10679, u}
with
  (α : ∀ (α : Type (max u ?u.10680)), Small.{max u ?u.10680, max u ?u.10680} α) →
    (∀ (α : Type (max u ?u.10680)), Small.{max u ?u.10680, max u ?u.10680} α) α

in the last line? any idea for this?

[Shanghe Chen]

I read some discussion in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.233463.20universe.20constraint.20issues and https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/TypeMax.html#TypeMax But still no idea why it happened

[Joël Riou]

On my computer, I do not get any error...

[Kyle Miller]

Universe constraint solving has changed a bit in Lean 4.8.0-rc1. Are you on a mathlib more recent than May 2?

[Shanghe Chen]

I am in windows 10, Lean 4.6.0-rc1 and commit 0a4873b of MIL (I am doing some extra exercises my local copy of MIL)

[Shanghe Chen]

Glad to hear that it works somewhere :smiling_face: I am updating my local toolchain and fetching the last update of MIL user repo to see if it resolved in my environment or not

[Shanghe Chen]

It works now :tada:(Now I am in 4.8.0-rc1 with latest MIL) it’s also possible that I changed the local mathlib copy accidentally, when I run lake exec cache get there’s a message saying some files are not downloaded. After running git pull and deleting the directories .lake and lake-package and run lake exec cache get it reports no error now

[Shanghe Chen]

328DA930-68AA-4FEE-AFFB-9201E13F0586.jpg

[Shanghe Chen]

Thank you for the kindly help :blush:

[Avi Craimer]

Hi,

I am having similar problem. I just updated with elan to v4.8 but I'm still getting the error so I probably need to specify the universe levels manually somehow.

I'm building an inductive type for mathematical relations. I want to allow the domain and codomain of the relation to originate in different type universes, but since relations are reversible (converse) I may need to lift both types to the max of the two universes. I'm not sure how to do this.

inductive Relation :  (Dom : Type _) -> (Cod : Type _) -> Type _
-- universe error occurs in the `first` constructor
| first (α) ( β) : Relation (α × β) α

Full code here

Error message:

stuck at solving universe constraint
  max (?u.176+1) (?u.177+1) =?= max (max (?u.176+1) (?u.177+1)) (?u.242+1)
while trying to unify
  Type (max ?u.177 ?u.176) : Type ((max ?u.177 ?u.176) + 1)
with
  Type (max (max ?u.176 ?u.177) ?u.242) : Type (max ((max ?u.176 ?u.177) + 1) (?u.242 + 1))

Lean 4
β : Type ?u.242

[Shanghe Chen]

Hi maybe extracting a #MWE here would help?

[Bbbbbbbbba]

Not directly relevant, but in the full code you linked you have import MathLib.Tactic instead of import Mathlib.Tactic, and I think the former only works on case-insensitive file systems (as I learned when I myself tried to make my first mwe)

[Bbbbbbbbba]

So the thing is that first only makes sense when the Dom is in a higher universe than Cod, right?

[Avi Craimer]

Ok, I got it working now. So I think that Dom and Cod have to be in the same type universe since .converse switches the order.

Here is the working code.
https://github.com/AviCraimer/lean-math-logic-exploration/blob/main/LeanMathLogicExploration/RelationalAlgebra.lean

The main thing I learned was how to lift the type universe to make certain relations where the Cod and Dom start out in different universes.

For example, a relation that represents the evaluation function (i.e., it maps a relation expression to its set of Pairs).

def Relation.evalRel  {α β : Type u}  : Relation (Relation α β) (PLift (Relation.Pairs α  β)) :=
  atomic fun (R:Relation α β) (f: PLift (Pairs α β) ) =>
    let evaluatedR := PLift.up (Relation.eval R)
  evaluatedR = f

I needed to use PLift here so that it would type check. I suppose this could be automated somehow.