Zulip Chat Archive

Stream: general

Topic: Universes for categories of categories


Kind Bubble (Jan 10 2023 at 20:39):

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 (Jan 10 2023 at 20:42):

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

Eric Wieser (Jan 10 2023 at 20:43):

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

Notification Bot (Jan 10 2023 at 20:45):

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

Eric Wieser (Jan 10 2023 at 20:48):

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 (Jan 10 2023 at 20:53):

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) : xx := PSigma.mk (Eq.refl x) Unit.unit /-to go-/
def Symm {X : Type _} {x : X} {y : X} (f:Σ'(_ : x = y),Unit):(yx) := 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) : (xz):= 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:xy) : (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 (Jan 10 2023 at 21:00):

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

Eric Wieser (Jan 10 2023 at 21:01):

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

Eric Wieser (Jan 10 2023 at 21:03):

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

Kind Bubble (Jan 10 2023 at 21:17):

Wow thanks a ton.

Kind Bubble (Jan 10 2023 at 21:18):

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 (Jan 10 2023 at 21:19):

You can name your universes. Before the structure, type

universe u

then replace Type _ with Type u.

Sky Wilshaw (Jan 10 2023 at 21:20):

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 (Jan 10 2023 at 21:20):

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 (Jan 10 2023 at 21:21):

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

Sky Wilshaw (Jan 10 2023 at 21:21):

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

Kind Bubble (Jan 10 2023 at 21:22):

Thanks!

Kind Bubble (Jan 10 2023 at 21:25):

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 (Jan 10 2023 at 21:26):

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 (Jan 10 2023 at 21:27):

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

Sky Wilshaw (Jan 10 2023 at 21:27):

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

Kind Bubble (Jan 10 2023 at 21:43):

Wow thanks so helpful Sky.

Kevin Buzzard (Jan 11 2023 at 08:47):

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 (Oct 30 2023 at 19:10):

@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.


Last updated: Dec 20 2023 at 11:08 UTC