# Zulip Chat Archive

## Stream: new members

### Topic: type expected error

#### Calle Sönne (Dec 02 2019 at 14:14):

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 (Dec 02 2019 at 14:17):

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 (Dec 02 2019 at 14:18):

Lean complains `F.map k.f.op`

is a function instead of being a type.

#### Patrick Massot (Dec 02 2019 at 14:18):

What is the type you hope `id_prod_maps (X : C) (S : sieve X)`

will have?

#### Patrick Massot (Dec 02 2019 at 14:19):

Maybe you wrote Pi where you wanted lambda

#### Calle Sönne (Dec 02 2019 at 14:19):

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

#### Patrick Massot (Dec 02 2019 at 14:19):

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

#### Patrick Massot (Dec 02 2019 at 14:20):

Ok, good.

#### Kevin Buzzard (Dec 02 2019 at 14:20):

Pi makes the types and lambda makes the terms

#### Calle Sönne (Dec 02 2019 at 14:20):

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

#### Patrick Massot (Dec 02 2019 at 14:21):

Pi is definitely a type maker.

#### Kevin Buzzard (Dec 02 2019 at 14:21):

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

#### Chris Hughes (Dec 02 2019 at 14:22):

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

That's what elements of Pi types do

#### Kevin Buzzard (Dec 02 2019 at 14:22):

Pi is like "forall".

#### Kevin Buzzard (Dec 02 2019 at 14:23):

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

Last updated: Dec 20 2023 at 11:08 UTC