maps out of dependent product

Stream: lean4

[Dean Young]

How might I construct a map out of a direct sum? For instance:

variable {X : Type}
variable {Y : Type}
variable {Z : Type}
variable {f : X -> Y}
variable {g : Z -> Y}

How might I construct a map out of:

def Sigma (x : X) => (Sigma (z : Z) =>  {u : Unit // f x = g z})

(I want to treat this like an inductive type).

[Kevin Buzzard]

You can't define Sigma in terms of Sigma.

[Scott Kovach]

if I understand correctly, I think you might have meant to write something like this:

variable {X : Type}
variable {Y : Type}
variable {Z : Type}
variable (f : X -> Y)
variable (g : Z -> Y)

def pullback := Sigma fun (x : X) => (Sigma fun (z : Z) => {u : Unit // f x = g z})
def pullback' := Σ' x z, f x = g z -- see PSigma

example : pullback (id : ℕ → ℕ) id → ℕ
| ⟨x, z, h⟩ => x

if your real example is more complicated, it might be better to define your own structure

structure pullback'' (α β γ) (f : α → γ) (g : β → γ) where
  a : α
  b : β
  h : f a = g b