309f44d007
This PR improves universe level inference for the `inductive` and `structure` commands to be more reliable and to produce better error messages. Recall that the main constraint for inductive types is that if `u` is the universe level for the type and `u > 0`, then each constructor field's universe level `v` satisfies `v ≤ u`, where a *constructor field* is an argument that is not one of the type's *parameters* (recall: the type's parameters are a prefix of the parameters shared by the type former and all the constructors). Given this constraint, the `inductive` elaborator attempts to find reasonable assignments to metavariables that may be present: - For the universe level `u`, choosing an assignment that makes this level least is reasonable, provided it is unique. - For constructor fields, choosing the unique assignment is usually reasonable. - For the type's parameters, promoting level metavariables to new universe level parameters is reasonable. The order of these steps led to somewhat convoluted error messages; for example, metavariable->parameter promotion was done early, leading to errors mentioning `u_1`, `u_2`, etc. instead of metavariables, as well as extraneous level constraint errors. Furthermore, early parameter promotion meant it was too late to perform certain kinds of inferences. Now there is a straightforward order of inference: 1. If the type's universe level could be zero, it checks that the type is an "obvious `Prop` candidate", which means it's non-recursive, has one constructor with at least one field, and all the fields are proofs. If it's a `Prop` candidate, the level is set to zero and we skip to step 4. 2. If the type's simplified universe level is of the form `?u + k`, it will accumulate level constraints to find a least upper bound solution for `?u`. To avoid sort polymorphism, it adds `1 ≤ ?u + k`, ensuring the result stays in `Type _`, or at least `Sort (max 1 _)`. It allows other metavariables to appear in the assignment for `?u`, provided they appear in the type former, or for `structure` in the `extends` clause. 3. If the type's simplified universe level is then of the form `r + k`, where `r` is a parameter, metavariable, or zero, then for every constructor field it will take the `v ≤ r + k` constraint and extract `?v ≤ r + k'` constraints. It will also *weakly* extract `1 ≤ ?v` constraints, using the observation that it's surprising if fields are automatically inferred to be proofs. Once the constraints are collected, each metavariable is solved for independently. Heuristically, if there is a unique non-constant solution we take that, or else a unique constant solution. 4. Any remaining level metavariables in the type former (or `extends` clause) become level parameters. 5. Remaining level metavariables in the constructor fields are reported as errors. 6. Then, the elaborator checks that the level constraints actually hold and reports an error if they don't. In 2 and 3, there are procedures to simplify universe levels. You can write `Sort (max 1 _)` for the resulting type now and it will solve for `_`. The "accidentally higher universe" error is now a warning. The constraint solving is also done in a more careful way, which keeps it from being reported erroneously. There are still some erroneous reports, but these ones are hard for the checker to reject. As before, the warning can be turned off by giving an explicit universe. Note about `extends` clauses: in testing, there were examples where it was surprising if the universe polymorphism of parent structures didn't carry over to the type being defined, even though parent structures are actually constructor fields. **Breaking change.** Universe level metavariables present only in constructor fields are no longer promoted to be universe level parameters: use explicit universe level parameters. This promotion was inconsistently done depending on whether the inductive type's universe level had a metavariable, and also it caused confusion for users, since these universe levels are not constrained by the type former's parameters. **Breaking change.** Now recursive types do not count as "obvious `Prop` candidates". Use an explicit `Prop` type former annotation on recursive inductive predicates. Additional changes: - level metavariable errors are now localized to constructors, and `structure` fields have such errors localized to fields - adds module docs for the index promotion algorithm and the universe level inference algorithm for inductives - factors out `Lean.Elab.Term.forEachExprWithExposedLevelMVars` for printing out the context of an expression with universe level metavariables - makes universe level metavariable exposure more effective at exposing level metavariables (with an exception of `sorry` terms, which are too noisy to expose) Supersedes #11513 and #11524.
499 lines
12 KiB
Text
499 lines
12 KiB
Text
section Mathlib.CategoryTheory.ConcreteCategory.Bundled
|
||
|
||
universe u v
|
||
|
||
namespace CategoryTheory
|
||
|
||
variable {c : Type u → Type v}
|
||
|
||
structure Bundled (c : Type u → Type v) : Type max (u + 1) v where
|
||
α : Type u
|
||
str : c α := by infer_instance
|
||
|
||
set_option checkBinderAnnotations false in
|
||
def Bundled.of {c : Type u → Type v} (α : Type u) [str : c α] : Bundled c :=
|
||
⟨α, str⟩
|
||
|
||
end CategoryTheory
|
||
|
||
end Mathlib.CategoryTheory.ConcreteCategory.Bundled
|
||
|
||
section Mathlib.Logic.Equiv.Defs
|
||
|
||
open Function
|
||
|
||
universe u v
|
||
|
||
variable {α : Sort u} {β : Sort v}
|
||
|
||
structure Equiv (α : Sort _) (β : Sort _) where
|
||
protected toFun : α → β
|
||
protected invFun : β → α
|
||
|
||
infixl:25 " ≃ " => Equiv
|
||
|
||
protected def Equiv.symm (e : α ≃ β) : β ≃ α := ⟨e.invFun, e.toFun⟩
|
||
|
||
end Mathlib.Logic.Equiv.Defs
|
||
|
||
section Mathlib.Combinatorics.Quiver.Basic
|
||
|
||
universe v v₁ v₂ u u₁ u₂
|
||
|
||
class Quiver (V : Type u) where
|
||
Hom : V → V → Sort v
|
||
|
||
infixr:10 " ⟶ " => Quiver.Hom
|
||
|
||
structure Prefunctor (V : Type u₁) [Quiver.{v₁} V] (W : Type u₂) [Quiver.{v₂} W] where
|
||
obj : V → W
|
||
map : ∀ {X Y : V}, (X ⟶ Y) → (obj X ⟶ obj Y)
|
||
|
||
end Mathlib.Combinatorics.Quiver.Basic
|
||
|
||
section Mathlib.CategoryTheory.Category.Basic
|
||
|
||
universe v u
|
||
|
||
namespace CategoryTheory
|
||
|
||
class CategoryStruct (obj : Type u) : Type max u (v + 1) extends Quiver.{v + 1} obj where
|
||
id : ∀ X : obj, Hom X X
|
||
comp : ∀ {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
|
||
|
||
scoped notation "𝟙" => CategoryStruct.id
|
||
scoped infixr:80 " ≫ " => CategoryStruct.comp
|
||
|
||
class Category (obj : Type u) : Type max u (v + 1) extends CategoryStruct.{v} obj where
|
||
|
||
end CategoryTheory
|
||
|
||
end Mathlib.CategoryTheory.Category.Basic
|
||
|
||
section Mathlib.CategoryTheory.Functor.Basic
|
||
|
||
namespace CategoryTheory
|
||
|
||
universe v v₁ v₂ v₃ u u₁ u₂ u₃
|
||
|
||
structure Functor (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D] : Type max v₁ v₂ u₁ u₂
|
||
extends Prefunctor C D where
|
||
|
||
infixr:26 " ⥤ " => Functor
|
||
|
||
namespace Functor
|
||
|
||
section
|
||
|
||
variable (C : Type u₁) [Category.{v₁} C]
|
||
|
||
protected def id : C ⥤ C where
|
||
obj X := X
|
||
map f := f
|
||
|
||
notation "𝟭" => Functor.id
|
||
|
||
variable {C}
|
||
|
||
theorem id_obj (X : C) : (𝟭 C).obj X = X := rfl
|
||
|
||
theorem id_map {X Y : C} (f : X ⟶ Y) : (𝟭 C).map f = f := rfl
|
||
|
||
end
|
||
|
||
variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
|
||
{E : Type u₃} [Category.{v₃} E]
|
||
|
||
def comp (F : C ⥤ D) (G : D ⥤ E) : C ⥤ E where
|
||
obj X := G.obj (F.obj X)
|
||
map f := G.map (F.map f)
|
||
|
||
@[simp] theorem comp_obj (F : C ⥤ D) (G : D ⥤ E) (X : C) : (F.comp G).obj X = G.obj (F.obj X) := rfl
|
||
|
||
infixr:80 " ⋙ " => Functor.comp
|
||
|
||
theorem comp_map (F : C ⥤ D) (G : D ⥤ E) {X Y : C} (f : X ⟶ Y) :
|
||
(F ⋙ G).map f = G.map (F.map f) := rfl
|
||
|
||
end Functor
|
||
|
||
end CategoryTheory
|
||
|
||
end Mathlib.CategoryTheory.Functor.Basic
|
||
|
||
section Mathlib.CategoryTheory.NatTrans
|
||
|
||
namespace CategoryTheory
|
||
|
||
universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄
|
||
|
||
variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
|
||
|
||
structure NatTrans (F G : C ⥤ D) : Type max u₁ v₂ where
|
||
app : ∀ X : C, F.obj X ⟶ G.obj X
|
||
naturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.map f ≫ app Y = app X ≫ G.map f
|
||
|
||
namespace NatTrans
|
||
|
||
/-- `NatTrans.id F` is the identity natural transformation on a functor `F`. -/
|
||
protected def id (F : C ⥤ D) : NatTrans F F where
|
||
app X := 𝟙 (F.obj X)
|
||
naturality := sorry
|
||
|
||
variable {F G H : C ⥤ D}
|
||
|
||
def vcomp (α : NatTrans F G) (β : NatTrans G H) : NatTrans F H where
|
||
app X := α.app X ≫ β.app X
|
||
naturality := sorry
|
||
|
||
end NatTrans
|
||
|
||
end CategoryTheory
|
||
|
||
|
||
end Mathlib.CategoryTheory.NatTrans
|
||
|
||
section Mathlib.CategoryTheory.Functor.Category
|
||
|
||
namespace CategoryTheory
|
||
|
||
universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄
|
||
|
||
variable (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]
|
||
|
||
variable {C D}
|
||
|
||
instance Functor.category : Category.{max u₁ v₂} (C ⥤ D) where
|
||
Hom F G := NatTrans F G
|
||
id F := NatTrans.id F
|
||
comp α β := NatTrans.vcomp α β
|
||
|
||
end CategoryTheory
|
||
|
||
end Mathlib.CategoryTheory.Functor.Category
|
||
|
||
section Mathlib.CategoryTheory.EqToHom
|
||
|
||
universe v₁ u₁
|
||
|
||
namespace CategoryTheory
|
||
|
||
variable {C : Type u₁} [Category.{v₁} C]
|
||
|
||
def eqToHom {X Y : C} (p : X = Y) : X ⟶ Y := by rw [p]; exact 𝟙 _
|
||
|
||
end CategoryTheory
|
||
|
||
end Mathlib.CategoryTheory.EqToHom
|
||
|
||
section Mathlib.CategoryTheory.Functor.Const
|
||
|
||
universe v₁ v₂ v₃ u₁ u₂ u₃
|
||
|
||
open CategoryTheory
|
||
|
||
namespace CategoryTheory.Functor
|
||
|
||
variable (J : Type u₁) [Category.{v₁} J]
|
||
variable {C : Type u₂} [Category.{v₂} C]
|
||
|
||
def const : C ⥤ J ⥤ C where
|
||
obj X :=
|
||
{ obj := fun _ => X
|
||
map := fun _ => 𝟙 X }
|
||
map f := { app := fun _ => f, naturality := sorry }
|
||
|
||
end CategoryTheory.Functor
|
||
|
||
|
||
end Mathlib.CategoryTheory.Functor.Const
|
||
|
||
section Mathlib.CategoryTheory.DiscreteCategory
|
||
|
||
namespace CategoryTheory
|
||
|
||
universe v₁ v₂ v₃ u₁ u₁' u₂ u₃
|
||
|
||
structure Discrete (α : Type u₁) where
|
||
as : α
|
||
|
||
abbrev SmallCategory (C : Type u) : Type (u + 1) := Category.{u} C
|
||
|
||
instance discreteCategory (α : Type u₁) : SmallCategory (Discrete α) where
|
||
Hom X Y := ULift (PLift (X.as = Y.as))
|
||
id _ := ULift.up (PLift.up rfl)
|
||
comp {X Y Z} g f := by
|
||
cases X
|
||
cases Y
|
||
cases Z
|
||
rcases f with ⟨⟨⟨⟩⟩⟩
|
||
exact g
|
||
|
||
namespace Discrete
|
||
|
||
variable {α : Type u₁}
|
||
|
||
theorem eq_of_hom {X Y : Discrete α} (i : X ⟶ Y) : X.as = Y.as :=
|
||
i.down.down
|
||
|
||
protected abbrev eqToHom {X Y : Discrete α} (h : X.as = Y.as) : X ⟶ Y :=
|
||
eqToHom sorry
|
||
|
||
variable {C : Type u₂} [Category.{v₂} C]
|
||
|
||
def functor {I : Type u₁} (F : I → C) : Discrete I ⥤ C where
|
||
obj := F ∘ Discrete.as
|
||
map {X Y} f := by
|
||
dsimp
|
||
rcases f with ⟨⟨h⟩⟩
|
||
exact eqToHom (congrArg _ h)
|
||
|
||
end Discrete
|
||
|
||
end CategoryTheory
|
||
|
||
|
||
end Mathlib.CategoryTheory.DiscreteCategory
|
||
|
||
section Mathlib.CategoryTheory.Types
|
||
|
||
namespace CategoryTheory
|
||
|
||
universe v v' w u u'
|
||
|
||
instance types : Category (Type u) where
|
||
Hom a b := a → b
|
||
id _ := id
|
||
comp f g := g ∘ f
|
||
|
||
end CategoryTheory
|
||
|
||
end Mathlib.CategoryTheory.Types
|
||
|
||
section Mathlib.CategoryTheory.Bicategory.Basic
|
||
|
||
namespace CategoryTheory
|
||
|
||
universe w v u
|
||
|
||
open Category
|
||
|
||
class Bicategory (B : Type u) extends CategoryStruct.{v} B where
|
||
homCategory : ∀ a b : B, Category.{w} (a ⟶ b) := by infer_instance
|
||
|
||
end CategoryTheory
|
||
|
||
end Mathlib.CategoryTheory.Bicategory.Basic
|
||
|
||
section Mathlib.CategoryTheory.Bicategory.Strict
|
||
|
||
namespace CategoryTheory
|
||
|
||
universe w v u
|
||
|
||
variable (B : Type u) [Bicategory.{w, v} B]
|
||
|
||
instance (priority := 100) StrictBicategory.category : Category B where
|
||
|
||
end CategoryTheory
|
||
|
||
end Mathlib.CategoryTheory.Bicategory.Strict
|
||
|
||
section Mathlib.CategoryTheory.Category.Cat
|
||
|
||
universe v u
|
||
|
||
namespace CategoryTheory
|
||
|
||
open Bicategory
|
||
|
||
def Cat :=
|
||
Bundled Category.{v, u}
|
||
|
||
namespace Cat
|
||
|
||
instance : CoeSort Cat (Type u) :=
|
||
⟨Bundled.α⟩
|
||
|
||
instance str (C : Cat.{v, u}) : Category.{v, u} C :=
|
||
Bundled.str C
|
||
|
||
def of (C : Type u) [Category.{v} C] : Cat.{v, u} :=
|
||
Bundled.of C
|
||
|
||
instance bicategory : Bicategory.{max v u, max v u} Cat.{v, u} where
|
||
Hom C D := C ⥤ D
|
||
id C := 𝟭 C
|
||
comp F G := F ⋙ G
|
||
homCategory := fun _ _ => Functor.category
|
||
|
||
@[simp] theorem of_α (C) [Category C] : (of C).α = C := rfl
|
||
|
||
def objects : Cat.{v, u} ⥤ Type u where
|
||
obj C := C
|
||
map F := F.obj
|
||
|
||
instance (X : Cat.{v, u}) : Category (objects.obj X) := (inferInstance : Category X)
|
||
|
||
end Cat
|
||
|
||
def typeToCat : Type u ⥤ Cat where
|
||
obj X := Cat.of (Discrete X)
|
||
map := fun {X} {Y} f => by
|
||
exact Discrete.functor (Discrete.mk ∘ f)
|
||
|
||
@[simp] theorem typeToCat_obj (X : Type u) : typeToCat.obj X = Cat.of (Discrete X) := rfl
|
||
@[simp] theorem typeToCat_map {X Y : Type u} (f : X ⟶ Y) :
|
||
typeToCat.map f = Discrete.functor (Discrete.mk ∘ f) := rfl
|
||
|
||
end CategoryTheory
|
||
|
||
|
||
end Mathlib.CategoryTheory.Category.Cat
|
||
|
||
section Mathlib.CategoryTheory.Adjunction.Basic
|
||
|
||
namespace CategoryTheory
|
||
|
||
open Category
|
||
|
||
universe v₁ v₂ v₃ u₁ u₂ u₃
|
||
|
||
variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
|
||
|
||
structure Adjunction (F : C ⥤ D) (G : D ⥤ C) where
|
||
unit : 𝟭 C ⟶ F.comp G
|
||
counit : G.comp F ⟶ 𝟭 D
|
||
|
||
infixl:15 " ⊣ " => Adjunction
|
||
|
||
namespace Adjunction
|
||
|
||
structure CoreHomEquivUnitCounit (F : C ⥤ D) (G : D ⥤ C) where
|
||
homEquiv : ∀ X Y, (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
|
||
unit : 𝟭 C ⟶ F ⋙ G
|
||
counit : G ⋙ F ⟶ 𝟭 D
|
||
homEquiv_counit : ∀ {X Y g}, (homEquiv X Y).symm.toFun g = F.map g ≫ counit.app Y
|
||
|
||
variable {F : C ⥤ D} {G : D ⥤ C}
|
||
|
||
def mk' (adj : CoreHomEquivUnitCounit F G) : F ⊣ G where
|
||
unit := adj.unit
|
||
counit := adj.counit
|
||
|
||
end Adjunction
|
||
|
||
end CategoryTheory
|
||
|
||
|
||
end Mathlib.CategoryTheory.Adjunction.Basic
|
||
|
||
section Mathlib.CategoryTheory.IsConnected
|
||
|
||
universe w₁ w₂ v₁ v₂ u₁ u₂
|
||
|
||
noncomputable section
|
||
|
||
open CategoryTheory.Category
|
||
|
||
namespace CategoryTheory
|
||
|
||
class IsPreconnected (J : Type u₁) [Category.{v₁} J] : Prop where
|
||
iso_constant :
|
||
∀ {α : Type u₁} (F : J ⥤ Discrete α) (j : J), False
|
||
|
||
class IsConnected (J : Type u₁) [Category.{v₁} J] : Prop extends IsPreconnected J where
|
||
[is_nonempty : Nonempty J]
|
||
|
||
variable {J : Type u₁} [Category.{v₁} J]
|
||
|
||
def Zag (j₁ j₂ : J) : Prop := sorry
|
||
|
||
def Zigzag : J → J → Prop := sorry
|
||
|
||
def Zigzag.setoid (J : Type u₂) [Category.{v₁} J] : Setoid J where
|
||
r := Zigzag
|
||
iseqv := sorry
|
||
|
||
end CategoryTheory
|
||
|
||
end
|
||
|
||
end Mathlib.CategoryTheory.IsConnected
|
||
|
||
section Mathlib.CategoryTheory.ConnectedComponents
|
||
|
||
universe v₁ v₂ v₃ u₁ u₂
|
||
|
||
noncomputable section
|
||
|
||
namespace CategoryTheory
|
||
|
||
variable {J : Type u₁} [Category.{v₁} J]
|
||
|
||
def ConnectedComponents (J : Type u₁) [Category.{v₁} J] : Type u₁ :=
|
||
Quotient (Zigzag.setoid J)
|
||
|
||
def Functor.mapConnectedComponents {K : Type u₂} [Category.{v₂} K] (F : J ⥤ K)
|
||
(x : ConnectedComponents J) : ConnectedComponents K :=
|
||
x |> Quotient.lift (Quotient.mk (Zigzag.setoid _) ∘ F.obj) sorry
|
||
|
||
def ConnectedComponents.functorToDiscrete (X : Type _)
|
||
(f : ConnectedComponents J → X) : J ⥤ Discrete X where
|
||
obj Y := Discrete.mk (f (Quotient.mk (Zigzag.setoid _) Y))
|
||
map g := Discrete.eqToHom sorry
|
||
|
||
def ConnectedComponents.liftFunctor (J) [Category J] {X : Type _} (F :J ⥤ Discrete X) :
|
||
(ConnectedComponents J → X) :=
|
||
Quotient.lift (fun c => (F.obj c).as) sorry
|
||
|
||
end CategoryTheory
|
||
|
||
end
|
||
|
||
end Mathlib.CategoryTheory.ConnectedComponents
|
||
|
||
universe v u
|
||
namespace CategoryTheory.Cat
|
||
|
||
variable (X : Type u) (C : Cat)
|
||
|
||
private def typeToCatObjectsAdjHomEquiv : (typeToCat.obj X ⟶ C) ≃ (X ⟶ Cat.objects.obj C) where
|
||
toFun f x := f.obj ⟨x⟩
|
||
invFun := Discrete.functor
|
||
|
||
private def typeToCatObjectsAdjCounitApp : (Cat.objects ⋙ typeToCat).obj C ⥤ C where
|
||
obj := Discrete.as
|
||
map := eqToHom ∘ Discrete.eq_of_hom
|
||
|
||
/-- `typeToCat : Type ⥤ Cat` is left adjoint to `Cat.objects : Cat ⥤ Type` -/
|
||
def typeToCatObjectsAdj : typeToCat ⊣ Cat.objects :=
|
||
Adjunction.mk' {
|
||
homEquiv := typeToCatObjectsAdjHomEquiv
|
||
unit := sorry
|
||
counit := {
|
||
app := typeToCatObjectsAdjCounitApp
|
||
naturality := sorry }
|
||
homEquiv_counit := by
|
||
intro X Y g
|
||
simp_all only [typeToCat_obj, Functor.id_obj, typeToCat_map, of_α, id_eq]
|
||
rfl }
|
||
|
||
def connectedComponents : Cat.{v, u} ⥤ Type u where
|
||
obj C := ConnectedComponents C
|
||
map F := Functor.mapConnectedComponents F
|
||
|
||
def connectedComponentsTypeToCatAdj : connectedComponents ⊣ typeToCat :=
|
||
Adjunction.mk' {
|
||
homEquiv := sorry
|
||
unit :=
|
||
{ app:= fun C ↦ ConnectedComponents.functorToDiscrete _ (𝟙 (connectedComponents.obj C))
|
||
naturality := by
|
||
intro X Y f
|
||
simp_all only [Functor.id_obj, Functor.comp_obj, typeToCat_obj, Functor.id_map,
|
||
Functor.comp_map, typeToCat_map, of_α, id_eq]
|
||
rfl }
|
||
counit := sorry
|
||
homEquiv_counit := sorry }
|
||
|
||
end CategoryTheory.Cat
|