Universes

Stream: general

[Kind Bubble]

Below I have a definition of category and a proof that the category of categories is a category... sort of. There's of course universe issues, which is maybe the most interesting part.

I want my definition of category to take in a universe. And I want to be able to express a strictly higher universe given any universe. That way, with my closed form Next_universe(Universe u) I can express that the category of categories is indeed a category... for any choice of universe to start with.

notation "Σ" "(" X ":" A ")" ":" F => Σ' (X : A), F
notation "Π" "(" X ":" A ")" ":" F => forall (X : A), F
notation "("  x  ":"  X  ")" "↦" F => (fun (x : X) => F)
notation "*" => Unit.unit
notation "⊛" => Unit
notation x "≡" y => Σ(_:x=y):⊛
def Refl {X : Type _} (x : X) : x≡x := PSigma.mk (Eq.refl x) *
def Symm {X : Type _} {x : X} {y : X} (f:Σ(_ : x = y):⊛):(y≡x) := PSigma.mk (Eq.symm f.1) *
notation "-" p => Symm p
def Trns {X : Type _} {x : X} {y : X} {z : X} (f : Σ(_ : x = y):⊛) (g : Σ(_ : y = z):⊛) : (x≡z):= PSigma.mk (Eq.trans f.1 g.1) *
notation p "~" q => Trns p q
def Push {X:Type _}{Y:Type _}{x:X}{y:X}(f:Π(_:X):Y)(p:x≡y) : (f x ≡ f y) := ⟨congrArg f p.1, *⟩
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):
⊛

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 /-REVISE-/

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) :=
Σ(FunObj : Π(_ : Obj C):Obj D):
Σ(FunHom : Π(X : Obj C):Π(Y : Obj C):Π(_ : Hom X Y):Hom (FunObj X) (FunObj Y)):
Σ(_ : Π(X : Obj C): FunHom X X (Idn X) ≡ Idn (FunObj X)):
Σ(_ : Π(X : Obj C):Π(Y : Obj C):Π(Z : Obj C):Π(f : Hom X Y):Π(g : Hom Y Z):Cmp (FunHom X Y f) (FunHom Y Z g) ≡ FunHom X Z (Cmp f g)):
⊛

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 :=
⟨
(X : Obj C)↦X,
(X : Obj C)↦(Y : Obj C)↦(f : Hom X Y)↦f,
(X : Obj C)↦Refl (Idn X),
(X : Obj C)↦(Y : Obj C)↦(Z : Obj C)↦(f : Hom X Y)↦(g : Hom Y Z)↦Refl (Cmp f g),
*
⟩
def CatCmp (C : Cat) (D : Cat) (E : Cat) (F : CatHom C D) (G : CatHom D E) : (CatHom C E) :=
⟨
(X : Obj C)↦(G.1) ((F.1) X),
(X : Obj C)↦(Y : Obj C)↦(f : Hom X Y)↦(G.2.1) (F.1 X) (F.1 Y) ((F.2.1) X Y f),
(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)),
(X : Obj C)↦(Y : Obj C)↦(Z : Obj C)↦(f : Hom X Y)↦(g : Hom Y Z)↦
(
Trns
(CatHomCmp G  (F[f]) (F[g]))
(Push (G.2.1 (F[X]) (F[Z])) (CatHomCmp F f g))
),
*⟩

def CatId1 (C : Cat) (D : Cat) (F : CatHom C D) : ((CatCmp C D D) F (CatIdn D) ≡ F) := ⟨(Refl F).1, *⟩

def CatId2 (C : Cat) (D : Cat) (F : CatHom C D) : ((CatCmp C C D) (CatIdn C) F ≡ F) := ⟨(Refl F).1, *⟩

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

[Eric Wieser]

Are you deliberately using Sigma for everything instead of structures? That would save you from all the .2.2.2.2.2 stuff

[Kind Bubble]

Yeah I wanted the Sigma and Product "purism".

[Kind Bubble]

is there such thing as a successor universe or something like that?

[Eric Wieser]

That "purism" (or perhaps moreso, the new notations you give it) makes it a lot harder for other people to read your code, which probably means fewer people will help out

[Eric Wieser]

I want my definition of category to take in a universe.

It already does; in fact, it takes two universes, one for each Type _

#check Cat
-- Cat.{u_1, u_2} : Type (max (u_1 + 1) (max 0 u_1 u_2) u_1 (u_2 + 1))

[Kind Bubble]

Ok let me fix up my notation and ask a different way - I want the category of categories to be a category and I suspect that will give me issues unless it just knows to pick a higher universe?

[Eric Wieser]

It will be easier to help you if you have code that demonstrates a problem with an error rather than code that doesn't yet have a problem

[Kind Bubble]

Thanks for all your help. I'm a bit new so I'm getting used to things.

One question is how to show equality of structures using equality of the constituents:

variable {X : Type}
variable {x : X}
variable {y: X}
variable {p : x = y}
structure Example where
    Z : Type _
    z : Z
def A:= { Z := X, z := x : Example}
def B := {Z := X, z := y : Example}
def AequalsB : A = B := sorry

[Junyan Xu]

I looked up docs#category_theory.Cat in mathlib and found its type is currently Type (max (u+1) u (v+1)), which is obviously not ideal and should be ascribed as Type (max (u+1) (v+1)) ...

[Junyan Xu]

You can check TPIL (7.8. Axiomatic Details) which anwsers the question

Since an inductive type lives in Sort u for some u, it is reasonable to ask which universe levels u can be instantiated to.

(Both structures and sigma types are implemented as inductive types)
(I should probably provide a Lean 4 reference, but I'm not familiar with them...)

[Junyan Xu]

One question is how to show equality of structures using equality of the constituents:

As for this question, Lean reports some errors as it parses your code:

variable {X : Type}
variable {x : X}
variable {y: X}
variable {p : x = y} -- if I comment this out then the error below doesn't occur; not sure why
structure Example where -- (kernel) declaration has free variables 'Example.mk.injEq'
    Z : Type _
    z : Z

def A:= { Z := X, z := x : Example}
def B := {Z := X, z := y : Example}
def AequalsB : A = B := sorry /- don't know how to synthesize implicit argument
  this is because `A` is a function of `X` and `x` and similarly for `B`; you need to
  write `@A X x = @B X y`. But actually it's the same as `@A X x = @A X y`, since
  `A` is the same as `B`: -/
example : @A = @B := rfl

And here are some solutions to the problem after making some corrections:

structure Example where
    Z : Type _
    z : Z

variable {X : Type} {x y : X} {p : x = y}

def A:= { Z := X, z := x : Example}
def B := {Z := X, z := y : Example}

lemma AequalsB : @A X x = @B X y := by
  rw [A, B, p]

lemma AequalsB' : @A X x = @B X y := by
  congr -- also works

lemma AequalsB'' : @A X x = @B X y := by
  ext /- if you add `@[ext]` before `structure Example`, `ext` here
    generates two goals `A.Z = B.Z` and `HEq A.z B.z`, but I don't recommend you
    deal with `HEq` as a beginner. -/