universe issues

Stream: general

[Eric Wieser]

Why does this work with a general ι, but fail with fin 2?

import data.fin

/-- A value which wraps a type. -/
inductive typeinfo (α : Type*) : Type
| of [] : typeinfo

/-- Get the type of the domain of a function type. -/
abbreviation {u} typeinfo.domain {α : Type u} {β : α → Type*}
  (a : typeinfo (Π (i : α), β i)) : Type u := α

/-- Get the type of the codomain of a function type. -/
abbreviation {u} typeinfo.codomain {α : Type*} {β : Type u}
  (a : typeinfo (α → β)) : Type u := β

/-- Get the type of the codomain of a dependent function type. -/
abbreviation {u} typeinfo.pi_codomain {α : Type*} {β : α → Type u}
  (a : typeinfo (Π (i : α), β i)) : α → Type u := β

variables {M' : Type*}  {ι : Type*}

#check (ι → M')
#check typeinfo (ι → M')
#check typeinfo.of (ι → M')
#check typeinfo.domain (typeinfo.of (ι → M'))

#check (fin 2 → M')
#check typeinfo (fin 2 → M')
#check typeinfo.of (fin 2 → M')
#check typeinfo.domain (typeinfo.of (fin 2 → M'))  -- fail, everything else works

[Chris Hughes]

The : _ trick works #check typeinfo.domain (typeinfo.of (fin 2 → M') : _). Not sure if that's helpful really though.

[Eric Wieser]

Unfortunately adding : _ in my larger context of using this for notation in #6152 makes it ineligible for pretty-printing

[Eric Wieser]

But it does fix the problem

[Eric Wieser]

attribute [elab_simple] typeinfo.of fixes it!

[Dean Young]

Does anyone know why I get this error from the code below?

Main.lean:177:34: error: function expected at
  category
term has type
  Type (?u.18181 + 1)
Main.lean:177:0: error: unused universe parameter 'u'

I'm trying to give one universe to "category" and an extra universe to "Cat" so that it can house the structures with the former universe level without any hassle going forward.

How do I define "Cat" here in a way which is consistent with

def n : Int := 1


def reflexivity {X : Type} {x : X} (p : x = x) := Eq.refl p


def symmetry {X : Type} {x : X} {y : X}  (p : x = y) := Eq.symm p


def transitivity {X : Type} {x : X} {y : X} {z : X} (p : x = y) (q : y = z) := Eq.trans p q


def extensionality (f g : X → Y) (p : (x:X) → f x = g x) : f = g := funext p


def equal_arguments {X : Type} {Y : Type} {a : X} {b : X} (f : X → Y) (p : a = b) : f a = f b := congrArg f p

def equal_functions {X : Type} {Y : Type} {f₁ : X → Y} {f₂ : X → Y} (p : f₁ = f₂) (x : X) : f₁ x = f₂ x := congrFun p x


-- A category C consists of:
structure category.{u} where
  Obj : Type u
  Hom : Obj → Obj → Type u
  Idn : (X:Obj) → Hom X X
  Cmp : (X:Obj) → (Y:Obj) → (Z:Obj) → (_:Hom X Y) → (_:Hom Y Z) → Hom X Z
  Id₁ : (X:Obj) → (Y:Obj) → (f:Hom X Y) →
    Cmp X Y Y f (Idn Y) = f
  Id₂ : (X:Obj) → (Y:Obj) → (f:Hom X Y) →
    Cmp X X Y (Idn X) f = f
  Ass : (W:Obj) → (X:Obj) → (Y:Obj) → (Z:Obj) → (f:Hom W X) → (g:Hom X Y) → (h:Hom Y Z) →
    (Cmp W X Z) f (Cmp X Y Z g h) = Cmp W Y Z (Cmp W X Y f g) h


-- Notation for the identity map which infers the category:
def identity_map (C : category) (X : C.Obj) := C.Idn X
notation "𝟙_(" C ")" => identity_map C

def Idn {C : category} (X : C.Obj) := C.Idn X
notation "𝟙" X => Idn X

-- Notation for composition which infers the category and objects:
def composition (C : category) {X : C.Obj} {Y : C.Obj} {Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z) : C.Hom X Z := C.Cmp X Y Z f g
notation g "∘_(" C ")" f => composition C f g

def Cmp {C : category} {X : C.Obj} {Y : C.Obj} {Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z) : C.Hom X Z := C.Cmp X Y Z f g
notation g "∘" f => Cmp f g

-- Notation for hom
def hom (C : category) (X : C.Obj) (Y : C.Obj) := C.Hom X Y
notation X "→_(" C ")" Y => hom C X Y


-- obtaining a morphism from an equality
def Map (C : category) {X : C.Obj} {Y : C.Obj} (p : X = Y) : C.Hom X Y := by
subst p
exact C.Idn X


-- definition of an isomorphism from X to Y
structure isomorphism {C : category} (X : C.Obj) (Y : C.Obj) where
  Fst : C.Hom X Y
  Snd : C.Hom Y X
  Id₁ : (C.Cmp X Y X Fst Snd) = C.Idn X
  Id₂ : (C.Cmp Y X Y Snd Fst) = C.Idn Y


-- notation for isomorphisms from X to Y (≅)
notation X "≅" Y => isomorphism X Y


-- defining the inverse of an isomorphism between objects X and Y
def inverse {C : category} {X : C.Obj} {Y : C.Obj} (f : X ≅ Y) : Y ≅ X := {Fst := f.Snd, Snd := f.Fst, Id₁ := f.Id₂, Id₂ := f.Id₁}


-- notation for inverse : isos from X to Y to isos from Y to X
notation f "⁻¹" => inverse f


-- definition of a functor
structure functor (C : category) (D : category) where
   Obj : ∀(_ : C.Obj),D.Obj
   Hom : ∀(X : C.Obj),∀(Y : C.Obj),∀(_ : C.Hom X Y),D.Hom (Obj X) (Obj Y)
   Idn : ∀(X : C.Obj),Hom X X (C.Idn X) = D.Idn (Obj X)
   Cmp : ∀(X : C.Obj),∀(Y : C.Obj),∀(Z : C.Obj),∀(f : C.Hom X Y),∀(g : C.Hom Y Z),
   D.Cmp (Obj X) (Obj Y) (Obj Z) (Hom X Y f) (Hom Y Z g) = Hom X Z (C.Cmp X Y Z f g)


-- notation for the type of Hom from a category C to a category D
-- notation C "→_(Cat)" D => functor C D


-- definition of the identity functor on objects
def CatIdnObj (C : category) :=
fun(X : C.Obj)=>
X

-- definition of the identity functor on morphisms
def CatIdnMor (C : category) :=
fun(X : C.Obj)=>
fun(Y : C.Obj)=>
fun(f : C.Hom X Y)=>
f

-- proving the identity law for the identity functor
def CatIdnIdn (C : category) :=
fun(X : C.Obj)=>
Eq.refl (C.Idn X)

-- proving the compositionality law for the identity functor
def CatIdnCmp (C : category) :=
fun(X : C.Obj)=>
fun(Y : C.Obj)=>
fun(Z : C.Obj)=>
fun(f : C.Hom X Y)=>
fun(g : C.Hom Y Z)=>
Eq.refl (C.Cmp X Y Z f g)

-- defining the identity functor
def CatIdn (C : category) : functor C C :=
{Obj := CatIdnObj C, Hom := CatIdnMor C, Idn := CatIdnIdn C, Cmp := CatIdnCmp C}


-- defining the composition G • F on objects
def CatCmpObj (C : category) (D : category) (E : category) (F : functor C D) (G : functor D E) :=
fun(X : C.Obj)=>
(G.Obj (F.Obj X))

-- defining the composition G • F on morphisms
def CatCmpHom (C : category) (D : category) (E : category) (F : functor C D) (G : functor D E) :=
fun(X : C.Obj)=>
fun(Y : C.Obj)=>
fun(f : C.Hom X Y)=>
(G.Hom) (F.Obj X) (F.Obj Y) (F.Hom X Y f)

-- proving the identity law for the composition G • F
def CatCmpIdn (C : category) (D : category) (E : category) (F : functor C D) (G : functor D E) :=
fun(X : C.Obj)=>
Eq.trans (congrArg (G.Hom (F.Obj X) (F.Obj X)) (F.Idn X) ) (G.Idn (F.Obj X))

-- proving the compositionality law for the composition G • F
def CatCmpCmp (C : category) (D : category) (E : category) (F : functor C D) (G : functor D E) :=
fun(X : C.Obj)=>
fun(Y : C.Obj)=>
fun(Z : C.Obj)=>
fun(f : C.Hom X Y)=>
fun(g : C.Hom Y Z)=>
((Eq.trans)
(G.Cmp (F.Obj X) (F.Obj Y) (F.Obj Z) (F.Hom X Y f) (F.Hom Y Z g))
(congrArg (G.Hom  (F.Obj X) (F.Obj Z)) (F.Cmp X Y Z f g)))

-- defining the composition in the category Cat
def CatCmp (C : category) (D : category) (E : category) (F : functor C D) (G : functor D E) : functor C E :=
{Obj := CatCmpObj C D E F G, Hom := CatCmpHom C D E F G,Idn := CatCmpIdn C D E F G, Cmp := CatCmpCmp C D E F G}


-- notation for the composition in the category Cat
def functor_composition {C : category} {D : category} {E : category} (F : functor C D) (G : functor D E) : functor C E := CatCmp C D E F G
notation G "∘_Cat" F => functor_composition F G


-- proving Cat.Id₁
def CatId₁ (C : category) (D : category) (F : functor C D) : ((CatCmp C D D) F (CatIdn D) = F) := Eq.refl F


-- Proof of Cat.Id₂
def CatId₂ (C : category) (D : category) (F : functor C D) : ((CatCmp C C D) (CatIdn C) F = F) := Eq.refl F


-- Proof of Cat.Ass
def CatAss (B : category) (C : category) (D : category) (E : category) (F : functor B C) (G : functor C D) (H : functor D E) : (CatCmp B C E F (CatCmp C D E G H) = CatCmp B D E (CatCmp B C D F G) H) :=
Eq.refl (CatCmp B C E F (CatCmp C D E G H))


-- The category of categories
def Cat.{u} : category := {Obj := category u, Hom := functor, Idn := CatIdn, Cmp := CatCmp, Id₁:= CatId₁, Id₂:= CatId₂, Ass := CatAss}

[Damiano Testa]

I do not know much about categories in Lean, but Cat : category := {Obj := category u, ...} seems suspicious: you are defining a term Cat or Type category and the object are category? This looks like the set of all sets...

[Eric Wieser]

Obj := category u is nonsense, it should be Obj := category.{u}

[Dean Young]

Thanks. How might I do .{u+1} -- just that? even though the definition of the category is already .{u}, like so:

-- A category C consists of:
structure category.{u} where
  Obj : Type u
  Hom : Obj → Obj → Type u
  Idn : (X:Obj) → Hom X X
  Cmp : (X:Obj) → (Y:Obj) → (Z:Obj) → (_:Hom X Y) → (_:Hom Y Z) → Hom X Z
  Id₁ : (X:Obj) → (Y:Obj) → (f:Hom X Y) →
    Cmp X Y Y f (Idn Y) = f
  Id₂ : (X:Obj) → (Y:Obj) → (f:Hom X Y) →
    Cmp X X Y (Idn X) f = f
  Ass : (W:Obj) → (X:Obj) → (Y:Obj) → (Z:Obj) → (f:Hom W X) → (g:Hom X Y) → (h:Hom Y Z) →
    (Cmp W X Z) f (Cmp X Y Z g h) = Cmp W Y Z (Cmp W X Y f g) h

[Eric Wieser]

Just that; but there's no need to

[Eric Wieser]

Lean will put the .{u+1} in automatically in the place that you need it to avoid the problem Damiano describes

[Dean Young]

Ok-- so it seems it can sometimes deduce what the universes should be but sometimes needs some help.