there is a small lemma in the HoTT book
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))
This proof is stated without proof so I thought it should be fairly easy to prove, but I just couldnt it.
My approach was first to use the Σ-encoding: (⟨ x , p ⟩ ≡ ⟨ x' , p' ⟩) ≃ (Σ[ γ ∈ (x ≡ x') ] ((transport γ (λ u → f u ≡ y) p) ≡ p'))
and finally to prove
(Σ[ γ ∈ (x ≡ x') ] ((transport γ (λ u → f u ≡ y) p) ≡ p')) ≃ (Σ[ γ ∈ (x ≡ x') ] ((cong f γ) ■ p' ≡ p))
to do that, it is enough to prove the second coordinates are isomorphic:
((transport γ (λ u → f u ≡ y) p) ≡ p') ≃ ((cong f γ) ■ p' ≡ p)
But this is an isomorphism between equality of paths. And is just too hard to prove.
Something like this defines a map from left to right:
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 γ))))
but then proving epi and mono is extremely hard. I think using path induction somewhere is the way to go but I cant find the right path induction. Any ideas??
By path induction on γ you reduce to showing that (p ≡ p') ≃ (refl ∙ p' ≡ p) which is easy path algebra.