Product types

Stream: new members

[Calle Sönne]

I need to define a type of the form (A x B) where B might differ depending on what term of A I pick. In my case I want to define something where the terms are of the form: ((Y : C), (f : Z ⟶ Y)) Where (Z : C) where C is a category and the arrow is hom. How would I go about doing this (is this even possible)?
hom is defined as a function:

class has_hom (obj : Type u) : Type (max u (v+1)) :=
(hom : obj → obj → Type v)

So I thought that I would be OK to define it as a subtype of (C x Type v) but this wont work as I came to realise my terms will have type Z ⟶ Y not Type v which is the type of Z ⟶ Y.

[Chris Hughes]

That's a Sigma type. It could also be done with a structure which would be preferable.

[Calle Sönne]

Thank you! I thought Sigma only could be used when a function had a "product" output where the 2nd type depended on the 1st.

[Calle Sönne]

I will try to define a structure then