type expected error

Stream: new members

[Calle Sönne]

I get the following error that I do not quite understand:

Code:

def id_prod_maps (X : C) (S : sieve.{v} X) := Π k : domain X S, F.map k.f.op

Error:

type expected at
  F.map (has_hom.hom.op.{v u} (k.f))
term has type
  F.obj (op.{u+1} X) ⟶ F.obj (op.{u+1} (k.Y))

I dont quite understand this error, terms of type F.obj (op.{u+1} X) ⟶ F.obj (op.{u+1} (k.Y)) is exactly what I want my function to return! Or is this error F.map complaining?

[Calle Sönne]

I should note that F.map is defined as:

structure functor (C : Type u₁) [category.{v₁} C] (D : Type u₂) [category.{v₂} D] :
  Type (max v₁ v₂ u₁ u₂) :=
(obj       : C → D)
(map       : Π {X Y : C}, (X ⟶ Y) → ((obj X) ⟶ (obj Y)))
(map_id'   : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X) . obviously)
(map_comp' : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = (map f) ≫ (map g) . obviously)

And considering the type in the error, F.obj (op.{u+1} X) ⟶ F.obj (op.{u+1} (k.Y)) it seems (to me) that functor.map does indeed return what it is supposed to

[Patrick Massot]

Lean complains F.map k.f.op is a function instead of being a type.

[Patrick Massot]

What is the type you hope id_prod_maps (X : C) (S : sieve X) will have?

[Patrick Massot]

Maybe you wrote Pi where you wanted lambda

[Calle Sönne]

Yes, that seems to be the problem. Thank you!

[Patrick Massot]

It's hard to tell without knowing what is the maths you want to formalize.

[Patrick Massot]

Ok, good.

[Kevin Buzzard]

Pi makes the types and lambda makes the terms

[Calle Sönne]

So Pi returns types? I thought it returned a term of a type that depends on input

[Patrick Massot]

Pi is definitely a type maker.

[Kevin Buzzard]

variables (X Y : Type)
#check Pi (x : X), Y -- X → Y : Type

[Chris Hughes]

I thought it returned a term of a type that depends on input

That's what elements of Pi types do

[Kevin Buzzard]

Pi is like "forall".

[Kevin Buzzard]

and lambda gives you the proof of "forall ..."