cat is not a valid field of structure cat

Stream: general

[Kind Bubble]

Here I've tried to define the category of categories. But I ran into an issue:

Main.lean:25:23: error: 'Cat' is not a field of structure 'Cat'

I guess a structure can't be comprised of itself?

See the last line for where the error occurs.

How might I work around this?

import Init.Data.ToString.Basic

universe u

structure Cat 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
  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 Cmp {C : Cat} {X : C.Obj} {Y : C.Obj} {Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z) := C.Cmp X Y Z f g

notation g "∘" f => Cmp f g

structure Fun (C : Cat) (D : Cat) where
   Obj : ∀(_ : C.Obj),D.Obj
   Mor : ∀(X : C.Obj),∀(Y : C.Obj),∀(_ : C.Hom X Y),D.Hom (Obj X) (Obj Y)
   Idn : ∀(X : C.Obj),Mor 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) (Mor X Y f) (Mor Y Z g) = Mor X Z (C.Cmp X Y Z (f) (g))

def CatIdn (C : Cat) : Fun C C :=
{Obj := fun(X : C.Obj)=>X, Mor := fun(X : C.Obj)=>fun(Y : C.Obj)=>fun(f : C.Hom X Y)=>f, Idn := fun(X : C.Obj)=>Eq.refl (C.Idn X),Cmp := 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)}

def CatCmp (C : Cat) (D : Cat) (E : Cat) (F : Fun C D) (G : Fun D E) : (Fun C E):=
{Obj := fun(X : C.Obj)=>(G.Obj (F.Obj X)),Mor := fun(X : C.Obj)=>fun(Y : C.Obj)=>fun(f : C.Hom X Y)=>(G.Mor) (F.Obj X) (F.Obj Y) ((F.Mor) X Y f),Idn := fun(X : C.Obj)=> ((Eq.trans) (congrArg (G.Mor (F.Obj X) (F.Obj X)) (F.Idn X) ) (G.Idn (F.Obj X))),Cmp := 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.Mor X Y f) (F.Mor Y Z g)) (congrArg (G.Mor (F.Obj X) (F.Obj Z)) (F.Cmp X Y Z f g)))}

def CatId1 (C : Cat) (D : Cat) (F : Fun C D) : ((CatCmp C D D) F (CatIdn D) = F) := Eq.refl F

def CatId2 (C : Cat) (D : Cat) (F : Fun C D) : ((CatCmp C C D) (CatIdn C) F = F) := Eq.refl F

def CatAss (B : Cat) (C : Cat) (D : Cat) (E : Cat) (F : Fun B C) (G : Fun C D) (H : Fun 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))

def Category : Cat := {Cat,Fun,CatIdn,CatCmp,CatId1,CatId2,CatAss}

[Kevin Buzzard]

As far as I know that's not valid syntax to make a structure instance? Oh -- this is lean 4? Then I'm not so sure. But it's still a pretty wacky way to do it. What happens if you try it the normal way? Obj := Cat etc.

[Kind Bubble]

Oh! It's just the wrong syntax haha. Ok thanks Professor.

[Junyan Xu]

I tried the code with the correct syntax (def Category : Cat where Obj := Cat ... or { Obj := Cat, ... } but Lean reports universe error. I realized the problem is that even though Cat is one universe higher, Fun is in the original universe, so you either need to allow different universes for Obj and Hom, or else need to specify the universe of Fun to be one higher.

[Junyan Xu]

something like

structure Fun (C : Cat.{u}) (D : Cat.{u}) : Type (u+1) where

[Kind Bubble]

thanks!