Divide and conquer for a dependent type

Stream: general

[Dean Young]

Can anyone fill in the sorry here?

-- f here resembles a function I have.
def f (X : Type) : Type := X × Bool

-- g here resembles a function I have.
def g (X : Type) : Type := X × Bool

-- p here resembles my proof that the two functions are equal on their values.
def p (X : Type) : f X = g X := by
unfold f
unfold g
rfl

def foo : (fun X => g X) = (fun X => f X) := by
sorry

[Adam Topaz]

Doesn’t rfl do it?

[Arthur Adjedj]

def foo : (fun X => g X) = (fun X => f X) := funext p

[Dean Young]

Thanks funext was what I wanted.