error: expected '}'

Stream: general

[Kind Bubble]

Does anyone know why the line with

Mor := fun(X : C.Obj)=>fun(Y : C.Obj)=>fun(f : C.Hom X Y)=>f,

gives me
Main.lean:41:0: error: expected '}'

universe u
structure Category 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 : Category} {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 Fun2 (C : Category) (D : Category) 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))
variable {C : Category}
def CatIdn : Fun2 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)=>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)=>Refl (C.Cmp X Y Z f g)}

[Damiano Testa]

I'm not at a computer, but the commas ending the lines look a little suspicious... :shrug:

[Kind Bubble]

oh that was it thanks

[Damiano Testa]

Sometimes, also missing whitespace at the beginning of each line can give weird error messages...

[Adam Topaz]

And spaces can really help with readability... anyway, you def of CatIdn is indeed missing a } to match your { on the Obj line.