如何用Agda证明HoTT书中的引理4.2.5？

我在《同伦型论》（HoTT）中遇到如下未给出证明的引理：

lemma-4-2-5 : ∀ {n m : Level} {A : Set n} {B : Set m} {f : A → B} {y : B} {(⟨ x , p ⟩) (⟨ x' , p' ⟩) : fiber-map f y} 
             → (⟨ x , p ⟩ ≡ ⟨ x' , p' ⟩) ≃ (Σ[ γ ∈ (x ≡ x') ] ((cong f γ) ■ p' ≡ p))

我的思路如下：

• 先利用Σ类型的路径编码，得到中间等价：

  (⟨ x , p ⟩ ≡ ⟨ x' , p' ⟩) ≃ (Σ[ γ ∈ (x ≡ x') ] ((transport γ (λ u → f u ≡ y) p) ≡ p'))
  

• 接下来需要证明以下两个Σ类型等价：

  (Σ[ γ ∈ (x ≡ x') ] ((transport γ (λ u → f u ≡ y) p) ≡ p')) ≃ (Σ[ γ ∈ (x ≡ x') ] ((cong f γ) ■ p' ≡ p))
  

• 这一步只需对任意γ : x ≡ x'，证明两个路径类型的同构：

  ((transport γ (λ u → f u ≡ y) p) ≡ p') ≃ ((cong f γ) ■ p' ≡ p)
  

我尝试定义了从左到右的映射T1：

T1 : ((transport γ (λ u → f u ≡ y) p) ≡ p') → ((cong f γ) ■ p' ≡ p)
T1 ω = (sym (transport-identity-type-const γ)) ■ 
      ((cong (λ v → transport (sym γ) (λ u → f u ≡ y) v) (sym ω)) ■ 
      ((cong (λ v → v p) (comp-transport (λ u → f u ≡ y) γ (sym γ))) ■ 
      (cong (λ v → transport v (λ u → f u ≡ y) p) (trans-p-sym-p≡refl γ))))

但证明该映射是单射和满射的过程难度极大。我认为应该使用路径归纳法，但找不到合适的切入点，希望得到指导。

内容的提问来源于stack exchange，提问作者Werner Germán Busch