Lawvere's fixed point theorem in agda

I was struggling to prove a more basic version of lawvere's fixed point theorem in agda. Precisely I am trying to figure out the proof for the bottom theorem.

surjective : {A : _} {B : _} → (A → B) → Set
surjective {B = B} f = (b : B) → ∃ λ a → f a ≡ b

fixedPoint : {A : _} → (A → A) -> Set
fixedPoint f = ∃ λ a → f a ≡ a

lawvere : {A : _} {B : _}
        → (ϕ : A → A → B) → (surjective ϕ) → (f : B → B) →
        fixedPoint f
lawvere = ?

General tips about how to approach similar proofs involving existentials would also be helpful.

I think my problem was hesitancy to use equational reasoning which I often have trouble with in agda. The solution I eventually found was:

lawvere : {A : _} {B : _}
        → (ϕ : A → A → B) → (surjective ϕ) → (f : B → B) →
        fixedPoint f
lawvere {A} {B} ϕ surj f = ϕ p p , sym proof
  where
    q = λ a → f (ϕ a a)
    p = Σ.fst (surj q)
    proof =
      begin
        ϕ p p
      ≡⟨ (cong-app (Σ.snd (surj q)) p) ⟩
        q p
      ≡⟨ refl ⟩
        (λ a → f (ϕ a a)) p
      ≡⟨ refl ⟩
        f (ϕ p p)
      ∎