how to define as unique thing having some property

Stream: new members

[Sifat]

I am trying to formalize a version of the Elementary Theory of the Category of Sets in lean and am having some trouble.

import category_theory.category.basic
open category_theory

universes u
variables {Sets : Type (u+1)} [large_category Sets] {X Y Z : Sets}

structure cartProd (X Y : Sets) :=
(carrier : Sets)
(fst : carrier ⟶ X)
(snd : carrier ⟶ Y)
(univ_map : ∀ (Z : Sets) (f : Z ⟶ X) (g : Z ⟶ Y), ∃! (h : Z ⟶ carrier), h ≫ fst = f ∧ h ≫ snd = g)
constant Prod (X Y : Sets) : cartProd X Y

Given f and g, I want to define <f, g> to be the unique map whose existence is stipulated by cartProd.univ_map. I was hoping someone here might shed some light on how to do this as all my attempts fail to compile :sweat_smile: