## Stream: general

### Topic: universe issues

#### Eric Wieser (Feb 10 2021 at 09:46):

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 (Feb 10 2021 at 10:34):

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

#### Eric Wieser (Feb 10 2021 at 10:39):

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

#### Eric Wieser (Feb 10 2021 at 10:56):

But it does fix the problem

#### Eric Wieser (Feb 10 2021 at 10:58):

attribute [elab_simple] typeinfo.of fixes it!

#### Kind Bubble (May 21 2023 at 16:53):

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 (May 21 2023 at 17:12):

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 (May 21 2023 at 18:03):

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

#### Kind Bubble (May 21 2023 at 19:11):

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 (May 21 2023 at 19:39):

Just that; but there's no need to

#### Eric Wieser (May 21 2023 at 19:39):

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

#### Kind Bubble (May 21 2023 at 19:41):

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

Last updated: Aug 03 2023 at 10:10 UTC