Universes for categories of categories

Stream: general

[Kind Bubble]

Here I established the definitions of category, functor, composition of functors, identity functor, and unit and associativity laws for this composition. Cat here (which is not a structure but a type) introduces two new universes.

In the final piece of code I try to establish that categories form a category but I run into universe issues.

My question is, how might I tweak this code so that:
1) Cat introduces only one new universe in which Obj and Hom X Y both reside
2) Categories (of universe level n) form a category (of universe level one up)

def Cat :=
Σ'(Obj:Type _),
Σ'(Hom:
   ∀(_:Obj),∀(_:Obj),(Type _)),
Σ'(Id:
   ∀(X:Obj),(Hom X X)),
Σ'(Cmp:
   ∀(X:Obj),∀(Y:Obj),∀(Z:Obj),
   ∀(_:Hom X Y),∀(_:Hom Y Z),(Hom X Z)),
Σ'(_:
   ∀(X:Obj),∀(Y:Obj),
   ∀(f:Hom X Y),(Cmp X Y Y) f (Id Y) ≡ f),
Σ'(_:
   ∀(X:Obj),∀(Y:Obj),
   ∀(f:Hom X Y),(Cmp X X Y) (Id X) f ≡ f),
Σ'(_:
   ∀(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),
Unit

def Obj (C : Cat) := C.1

def Hom {C : Cat }(X : Obj C)(Y : Obj C) := C.2.1 X Y

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

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

def Id1 {C : Cat} {X : Obj C} {Y : Obj C} (f : Hom X Y) := C.2.2.2.2.2.1 X Y f

def Id2 {C : Cat} {X : Obj C} {Y : Obj C} (f : Hom X Y) := C.2.2.2.2.1 X Y f

def Ass {C : Cat} {W : Obj C} {X : Obj C} {Y : Obj C} {Z : Obj C} (f : Hom W X) (g : Hom X Y) (h : Hom Y Z) := C.2.2.2.2.2.2.1 W X Y Z f g h
def CatHom (C : Cat) (D : Cat) :=
Σ'(CatHomObj :
   ∀(_ : Obj C),
   Obj D),
Σ'(CatHomHom :
   ∀(X : Obj C),
   ∀(Y : Obj C),
   ∀(_ : Hom X Y),
   Hom (CatHomObj X) (CatHomObj Y)),
Σ'(_ :
   ∀(X : Obj C),
   CatHomHom X X (Idn X) ≡ Idn (CatHomObj X)),
Σ'(_ :
   ∀(X : Obj C),
   ∀(Y : Obj C),
   ∀(Z : Obj C),
   ∀(f : Hom X Y),
   ∀(g : Hom Y Z),
   Cmp (CatHomHom X Y f) (CatHomHom Y Z g) ≡ CatHomHom X Z (Cmp f g)),
Unit

def CatHomObj {C : Cat} {D : Cat} (F : CatHom C D) (X : Obj C) := F.1 X
notation:99 F "[" X:100 "]" => CatHomObj F X

def CatHomHom {C : Cat} {D : Cat} {X : Obj C} {Y : Obj C} (F : CatHom C D) (f : Hom X Y) := F.2.1 X Y f
notation:89 F "[" f:90 "]" => CatHomHom F f

def CatHomIdn {C : Cat} {D : Cat} (F : CatHom C D) (X : Obj C) := F.2.2.1 X

def CatHomCmp {C : Cat} {D : Cat} {X : Obj C} {Y : Obj C} {Z : Obj C} (F : CatHom C D) (f : Hom X Y) (g : Hom Y Z) := F.2.2.2.1 X Y Z f g
def CatIdn (C : Cat) : CatHom C C :=
⟨
fun(X : Obj C)=>X,
fun(X : Obj C)=>fun(Y : Obj C)=>fun(f : Hom X Y)=>f,
fun(X : Obj C)=>Refl (Idn X),
fun(X : Obj C)=>fun(Y : Obj C)=>fun(Z : Obj C)=>fun(f : Hom X Y)=>fun(g : Hom Y Z)=>Refl (Cmp f g),
Unit.unit
⟩
def CatCmp (C : Cat) (D : Cat) (E : Cat) (F : CatHom C D) (G : CatHom D E) : (CatHom C E) :=
⟨
fun(X : Obj C)=>(G.1) ((F.1) X),
fun(X : Obj C)=>fun(Y : Obj C)=>fun(f : Hom X Y)=>(G.2.1) (F.1 X) (F.1 Y) ((F.2.1) X Y f),
fun(X : Obj C)=>Trns ( Push (G.2.1 (F.1 X) (F.1 X)) (F.2.2.1 X) ) ((G.2.2.1) (F.1 X)),
fun(X : Obj C)=>fun(Y : Obj C)=>fun(Z : Obj C)=>fun(f : Hom X Y)=>fun(g : Hom Y Z)=>
(
Trns
(CatHomCmp G  (F[f]) (F[g]))
(Push (G.2.1 (F[X]) (F[Z])) (CatHomCmp F f g))
),
Unit.unit⟩
def CatId1 (C : Cat) (D : Cat) (F : CatHom C D) : ((CatCmp C D D) F (CatIdn D) ≡ F) := ⟨(Refl F).1, Unit.unit⟩
def CatId2 (C : Cat) (D : Cat) (F : CatHom C D) : ((CatCmp C C D) (CatIdn C) F ≡ F) := ⟨(Refl F).1, Unit.unit⟩
def CatAss (B : Cat) (C : Cat) (D : Cat) (E : Cat) (F : CatHom B C) (G : CatHom C D) (H : CatHom D E) : (CatCmp B C E F (CatCmp C D E G H) ≡ CatCmp B D E (CatCmp B C D F G) H) := ⟨(Refl (CatCmp B C E F (CatCmp C D E G H))).1, Unit.unit ⟩

def Cat0 : Cat :=
⟨
Cat,
CatHom,
CatIdn,
CatCmp,
CatId1,
CatId2,
CatAss
⟩

[Notification Bot]

A message was moved here from #general > universe issues by Eric Wieser.

[Eric Wieser]

That code doesn't work for me as there's no ≡, Refl, or Trans

[Notification Bot]

15 messages were moved here from #general > Universes by Eric Wieser.

[Eric Wieser]

It's also worth remembering that even if you really want to stick to "sigma purity" you can write multiple binders after a sigma or forall:

def Cat := Σ'
  (Obj:Type _)
  (Hom: ∀(_:Obj) (_:Obj), (Type _))
  (Id: ∀ (X:Obj), (Hom X X))
  (Cmp: ∀ (X:Obj) (Y:Obj) (Z:Obj) (_:Hom X Y) (_:Hom Y Z), (Hom X Z))
  (_: ∀ (X:Obj) (Y:Obj) (f:Hom X Y), (Cmp X Y Y) f (Id Y) = f)
  (_: ∀ (X:Obj) (Y:Obj) (f:Hom X Y), (Cmp X X Y) (Id X) f = f)
  (_: ∀ (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),
Unit

[Kind Bubble]

Eric Wieser said:

It's also worth remembering that even if you really want to stick to "sigma purity" you can write multiple binders after a sigma or forall:

def Cat := Σ'
  (Obj:Type _)
  (Hom: ∀(_:Obj) (_:Obj), (Type _))
  (Id: ∀ (X:Obj), (Hom X X))
  (Cmp: ∀ (X:Obj) (Y:Obj) (Z:Obj) (_:Hom X Y) (_:Hom Y Z), (Hom X Z))
  (_: ∀ (X:Obj) (Y:Obj) (f:Hom X Y), (Cmp X Y Y) f (Id Y) = f)
  (_: ∀ (X:Obj) (Y:Obj) (f:Hom X Y), (Cmp X X Y) (Id X) f = f)
  (_: ∀ (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),
Unit

I haven't fully switched over but I did away with about half of the idiosyncrasies I had.

Ok here's the whole code for now. I'm sorry for the notation nuisance ... I'll probably switch over by the end of the day.

notation x "≡" y => Σ'(_:x=y),Unit
def Refl {X : Type _} (x : X) : x≡x := PSigma.mk (Eq.refl x) Unit.unit /-to go-/
def Symm {X : Type _} {x : X} {y : X} (f:Σ'(_ : x = y),Unit):(y≡x) := PSigma.mk (Eq.symm f.1) Unit.unit
notation "-" p => Symm p /-to go-/
def Trns {X : Type _} {x : X} {y : X} {z : X} (f : Σ'(_ : x = y),Unit) (g : Σ'(_ : y = z),Unit) : (x≡z):= PSigma.mk (Eq.trans f.1 g.1) Unit.unit
notation p "~" q => Trns p q /-to go-/
def Push {X:Type _}{Y:Type _}{x:X}{y:X}(f:∀(_:X),Y)(p:x≡y) : (f x ≡ f y) := ⟨congrArg f p.1, Unit.unit⟩ /-to go-/
structure Category where
  Obj : Type _
  Hom : ∀(_:Obj),∀(_:Obj), Type _
  Idn : ∀(X:Obj),Hom X X
  Cmp : ∀(X:Obj),∀(Y:Obj),∀(Z:Obj),∀(_:Hom X Y),∀(_:Hom Y Z),Hom X Z
  Id1 : ∀(X:Obj),∀(Y:Obj),∀(f:Hom X Y),(Cmp X Y Y) f (Idn Y) = f
  Id2 : ∀(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
def Cat :=
Σ'(Obj:Type _),
Σ'(Hom:
   ∀(_:Obj),∀(_:Obj),(Type _)),
Σ'(Id:
   ∀(X:Obj),(Hom X X)),
Σ'(Cmp:
   ∀(X:Obj),∀(Y:Obj),∀(Z:Obj),
   ∀(_:Hom X Y),∀(_:Hom Y Z),(Hom X Z)),
Σ'(_:
   ∀(X:Obj),∀(Y:Obj),
   ∀(f:Hom X Y),(Cmp X Y Y) f (Id Y) ≡ f),
Σ'(_:
   ∀(X:Obj),∀(Y:Obj),
   ∀(f:Hom X Y),(Cmp X X Y) (Id X) f ≡ f),
Σ'(_:
   ∀(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),
Unit

def Obj (C : Cat) := C.1

def Hom {C : Cat }(X : Obj C)(Y : Obj C) := C.2.1 X Y

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

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

def Id1 {C : Cat} {X : Obj C} {Y : Obj C} (f : Hom X Y) := C.2.2.2.2.2.1 X Y f

def Id2 {C : Cat} {X : Obj C} {Y : Obj C} (f : Hom X Y) := C.2.2.2.2.1 X Y f

def Ass {C : Cat} {W : Obj C} {X : Obj C} {Y : Obj C} {Z : Obj C} (f : Hom W X) (g : Hom X Y) (h : Hom Y Z) := C.2.2.2.2.2.2.1 W X Y Z f g h
def CatHom (C : Cat) (D : Cat) :=
Σ'(CatHomObj :
   ∀(_ : Obj C),
   Obj D),
Σ'(CatHomHom :
   ∀(X : Obj C),
   ∀(Y : Obj C),
   ∀(_ : Hom X Y),
   Hom (CatHomObj X) (CatHomObj Y)),
Σ'(_ :
   ∀(X : Obj C),
   CatHomHom X X (Idn X) ≡ Idn (CatHomObj X)),
Σ'(_ :
   ∀(X : Obj C),
   ∀(Y : Obj C),
   ∀(Z : Obj C),
   ∀(f : Hom X Y),
   ∀(g : Hom Y Z),
   Cmp (CatHomHom X Y f) (CatHomHom Y Z g) ≡ CatHomHom X Z (Cmp f g)),
Unit

def CatHomObj {C : Cat} {D : Cat} (F : CatHom C D) (X : Obj C) := F.1 X
notation:99 F "[" X:100 "]" => CatHomObj F X

def CatHomHom {C : Cat} {D : Cat} {X : Obj C} {Y : Obj C} (F : CatHom C D) (f : Hom X Y) := F.2.1 X Y f
notation:89 F "[" f:90 "]" => CatHomHom F f

def CatHomIdn {C : Cat} {D : Cat} (F : CatHom C D) (X : Obj C) := F.2.2.1 X

def CatHomCmp {C : Cat} {D : Cat} {X : Obj C} {Y : Obj C} {Z : Obj C} (F : CatHom C D) (f : Hom X Y) (g : Hom Y Z) := F.2.2.2.1 X Y Z f g
def CatIdn (C : Cat) : CatHom C C :=
⟨
fun(X : Obj C)=>X,
fun(X : Obj C)=>fun(Y : Obj C)=>fun(f : Hom X Y)=>f,
fun(X : Obj C)=>Refl (Idn X),
fun(X : Obj C)=>fun(Y : Obj C)=>fun(Z : Obj C)=>fun(f : Hom X Y)=>fun(g : Hom Y Z)=>Refl (Cmp f g),
Unit.unit
⟩
def CatCmp (C : Cat) (D : Cat) (E : Cat) (F : CatHom C D) (G : CatHom D E) : (CatHom C E) :=
⟨
fun(X : Obj C)=>(G.1) ((F.1) X),
fun(X : Obj C)=>fun(Y : Obj C)=>fun(f : Hom X Y)=>(G.2.1) (F.1 X) (F.1 Y) ((F.2.1) X Y f),
fun(X : Obj C)=>Trns ( Push (G.2.1 (F.1 X) (F.1 X)) (F.2.2.1 X) ) ((G.2.2.1) (F.1 X)),
fun(X : Obj C)=>fun(Y : Obj C)=>fun(Z : Obj C)=>fun(f : Hom X Y)=>fun(g : Hom Y Z)=>
(
Trns
(CatHomCmp G  (F[f]) (F[g]))
(Push (G.2.1 (F[X]) (F[Z])) (CatHomCmp F f g))
),
Unit.unit⟩
def CatId1 (C : Cat) (D : Cat) (F : CatHom C D) : ((CatCmp C D D) F (CatIdn D) ≡ F) := ⟨(Refl F).1, Unit.unit⟩
def CatId2 (C : Cat) (D : Cat) (F : CatHom C D) : ((CatCmp C C D) (CatIdn C) F ≡ F) := ⟨(Refl F).1, Unit.unit⟩
def CatAss (B : Cat) (C : Cat) (D : Cat) (E : Cat) (F : CatHom B C) (G : CatHom C D) (H : CatHom D E) : (CatCmp B C E F (CatCmp C D E G H) ≡ CatCmp B D E (CatCmp B C D F G) H) := ⟨(Refl (CatCmp B C E F (CatCmp C D E G H))).1, Unit.unit ⟩
def Cat0 : Cat :=
⟨
Cat,
CatHom,
CatIdn,
CatCmp,
CatId1,
CatId2,
CatAss
⟩

So what I'm wondering is about the last piece of code (which is what gives the error). I think it's because of the universe level.

[Eric Wieser]

Your problem is that your sigma stuff ends with Unit and you forgot to provide Unit.unit after associativity

[Eric Wieser]

And because of your use of nestedPsigma's instead of structure you get a really cryptic error message

[Eric Wieser]

The error is made worse by the fact you called your sigma binder _ instead of Assoc or whatever

[Kind Bubble]

Wow thanks a ton.

[Kind Bubble]

Ok here I've started to switch to structure:

structure Category where
  Obj : Type _
  Hom : ∀(_:Obj),∀(_:Obj), Type _
  Idn : ∀(X:Obj),Hom X X
  Cmp : ∀(X:Obj),∀(Y:Obj),∀(Z:Obj),∀(_:Hom X Y),∀(_:Hom Y Z),Hom X Z
  Id1 : ∀(X:Obj),∀(Y:Obj),∀(f:Hom X Y),(Cmp X Y Y) f (Idn Y) = f
  Id2 : ∀(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

How might I modify this structure so that it only introduces one universe? Notice that Obj and Hom each introduce their own. Or is it actually more efficient to keep them separate?

[Sky Wilshaw]

You can name your universes. Before the structure, type

universe u

then replace Type _ with Type u.

[Sky Wilshaw]

Note that in the case when you have function binders with anonymous names, you can use -> syntax.

Hom : Obj -> Obj -> Type u
Cmp : ∀ X Y Z, Hom X Y -> Hom Y Z -> Hom X Z

You can also use \to to get a nicer looking arrow.

[Kind Bubble]

Sky Wilshaw said:

You can name your universes. Before the structure, type

universe u

then replace Type _ with Type u.

can u be switched for any other universe somehow?

[Sky Wilshaw]

Your type becomes universe-polymorphic. You can instantiate Category with any concrete universe such as 0 or 2.

[Sky Wilshaw]

To be more precise, your type was already universe-polymorphic - you just didn't have names for the universe variables you created.

[Kind Bubble]

Thanks!

[Kind Bubble]

hmm ok. suppose I want to keep this category structure. A structure has type sort right? consider the Cat0 at the end of my code... that's my goal right now, is to obtain Cat0 like I have above but use structures where appropriate.

Right now I'm struggling with that since it seems like Cat can only take in an ordinary type e.g. for Objects. But Cat0 is supposed to take in Cat as objects, and Cat will be a structure.

[Sky Wilshaw]

The type of a structure depends on its fields, and you can generally make it whatever you like as long as you don't violate universe impredicativity. If your structure has a field of type Type u, then typically the structure lives in Type (u + 1).

[Sky Wilshaw]

You can check by typing (something like) #check Category.{0} and it'll tell you its type.

[Sky Wilshaw]

Since Category can be instantiated with any universe parameter, there should be no problem in writing the category of categories.

[Kind Bubble]

Wow thanks so helpful Sky.

[Kevin Buzzard]

There's a problem (Russell's paradox) writing the set of all sets in mathematics and there will be the same problem writing the category of all categories, which presumably will be solved here using universes.

[Dean Young]

@Kevin Buzzard

It's been a while since you said that but I think it could be helpful to illustrate a bit of a difference in perspective:

When I first ventured into computer proof assistants, I made myself a version of ETCC in Java using 0-cells (categories), 1-cells (functors), 2-cells (natural transformations), and 3-cells (equations), along with the facility of producing variables in each. Much as if these were inductive types in Lean 4, the 2-cells were particular two-dimensional arrays.

Inside that I put the Lawvere fixed point theorem and experimented separately with p ∧ ¬ p -- no mention of Russel.

So here is the alternative perspective: If Lean (with its tactical facility and so on) had not set up the universe hierarchy to my satisfaction, I would have found it no trouble to embed my ETCC into their Turing machines instead.