Home
module foundations.identity-type-respects-equivalence where
Imports
open import foundations.universe
open import foundations.identity-type
open import foundations.sigma-type
open import foundations.transport
open import foundations.bi-invertible-map
open import foundations.quasi-inverse-to-bi-invertible-map
open import foundations.function
open import foundations.homotopy
open import foundations.functions-are-functors
open import foundations.bi-invertible-map
open import foundations.groupoid-laws
open import foundations.identity-type-reasoning
open import foundations.quasi-inverse
open import foundations.bi-invertible-map-to-quasi-inverse
open import foundations.homotopies-are-natural-isomorphisms
private variable
ℓ : Level
A B : Type ℓ
idRespEquiv : ∀ (f : A → B) → biinv f
→ ∀ (x y : A) → biinv (λ (p : x ＝ y) → ap f p)
idRespEquiv f b x y = QuasiInv⇒biinv (record
{ g = λ p → sym (linv x) ∙ (ap g p ∙ linv y)
; linv = λ {refl → ap (sym (linv x) ∙_) (lunitId _) ∙ linvId _}
; rinv = zz
})
where
open QuasiInv (biinv⇒QuasiInv b)
zw : ∀ (p : f x ＝ f y)
→ ap (g ∘ f) (sym (linv x) ∙ (ap g p ∙ linv y)) ∙ linv y
＝ linv x ∙ (sym (linv x) ∙ (ap g p ∙ linv y))
zw p = sym (naturalityHtpy linv _) ∙ ap (linv x ∙_) (apId _)
zx : ∀ (p : f x ＝ f y)
→ ap (g ∘ f) (sym (linv x) ∙ (ap g p ∙ linv y))
＝ linv x ∙ ((sym (linv x) ∙ (ap g p ∙ linv y)) ∙ sym (linv y))
zx p = rcancelId _ _ (linv y) (
ap (g ∘ f) (sym (linv x) ∙ (ap g p ∙ linv y)) ∙ linv y
＝⟨ zw p ⟩
linv x ∙ (sym (linv x) ∙ (ap g p ∙ linv y))
＝⟨ sym (ap (linv x ∙_) (relimId _ _ (linvId _))) ⟩
linv x ∙ ((sym (linv x) ∙ (ap g p ∙ linv y)) ∙ (sym (linv y) ∙ linv y))
＝⟨ ap (linv x ∙_) (sym (assocId _ _ _)) ⟩
linv x ∙ (((sym (linv x) ∙ (ap g p ∙ linv y)) ∙ sym (linv y)) ∙ linv y)
＝⟨ sym (assocId _ _ _) ⟩
(linv x ∙ ((sym (linv x) ∙ (ap g p ∙ linv y)) ∙ sym (linv y))) ∙ linv y
∎)
zy : ∀ (p : f x ＝ f y)
→ rinv (f x) ∙ ap f (sym (linv x) ∙ (ap g p ∙ linv y)) ＝ rinv (f x) ∙ p
zy p =
rinv (f x) ∙ ap f (sym (linv x) ∙ (ap g p ∙ linv y))
＝⟨ ap (rinv (f x) ∙_) (sym (apId _)) ⟩
rinv (f x) ∙ ap (idFunction _) (ap f (sym (linv x) ∙ (ap g p ∙ linv y)))
＝⟨ naturalityHtpy rinv _ ⟩
ap (f ∘ g) (ap f (sym (linv x) ∙ (ap g p ∙ linv y))) ∙ rinv (f y)
＝⟨ ap (_∙ rinv (f y)) (apAp f (f ∘ g) _) ⟩
ap (f ∘ (g ∘ f)) (sym (linv x) ∙ (ap g p ∙ linv y)) ∙ rinv (f y)
＝⟨ ap (_∙ rinv (f y)) (sym (apAp (g ∘ f) f _)) ⟩
ap f (ap (g ∘ f) (sym (linv x) ∙ (ap g p ∙ linv y))) ∙ rinv (f y)
＝⟨ ap (_∙ rinv (f y)) (ap (ap f) (zx p)) ⟩
ap f (linv x ∙ ((sym (linv x) ∙ (ap g p ∙ linv y)) ∙ sym (linv y))) ∙ rinv (f y)
＝⟨ ap (_∙ rinv (f y)) (ap∙ f _ _) ⟩
(ap f (linv x) ∙ ap f ((sym (linv x) ∙ (ap g p ∙ linv y)) ∙ sym (linv y))) ∙ rinv (f y)
＝⟨ ap (λ w → (ap f (linv x) ∙ w) ∙ rinv (f y)) (ap∙ f _ _) ⟩
(ap f (linv x) ∙ (ap f (sym (linv x) ∙ (ap g p ∙ linv y)) ∙ ap f (sym (linv y)))) ∙ rinv (f y)
＝⟨ ap (λ w → (ap f (linv x) ∙ (w ∙ ap f (sym (linv y)))) ∙ rinv (f y)) (ap∙ f _ _) ⟩
(ap f (linv x) ∙ ((ap f (sym (linv x)) ∙ ap f (ap g p ∙ linv y)) ∙ ap f (sym (linv y)))) ∙ rinv (f y)
＝⟨ ap (_∙ rinv (f y)) (sym (assocId _ _ _)) ⟩
((ap f (linv x) ∙ (ap f (sym (linv x)) ∙ ap f (ap g p ∙ linv y))) ∙ ap f (sym (linv y))) ∙ rinv (f y)
＝⟨ ap (λ w → (w ∙ ap f (sym (linv y))) ∙ rinv (f y)) (sym (assocId _ _ _)) ⟩
(((ap f (linv x) ∙ ap f (sym (linv x))) ∙ ap f (ap g p ∙ linv y)) ∙ ap f (sym (linv y))) ∙ rinv (f y)
＝⟨ ap
(λ w →
((w ∙ ap f (ap g p ∙ linv y)) ∙ ap f (sym (linv y))) ∙ rinv (f y))
(sym (ap∙ f _ _)) ⟩
((ap f (linv x ∙ sym (linv x)) ∙ ap f (ap g p ∙ linv y)) ∙ ap f (sym (linv y))) ∙ rinv (f y)
＝⟨ ap (λ w → (w ∙ ap f (sym (linv y))) ∙ rinv (f y)) (lelimId _ _ (ap (ap f) (rinvId _))) ⟩
(ap f (ap g p ∙ linv y) ∙ ap f (sym (linv y))) ∙ rinv (f y)
＝⟨ ap (_∙ rinv (f y)) (sym (ap∙ f _ _)) ⟩
ap f ((ap g p ∙ linv y) ∙ (sym (linv y))) ∙ rinv (f y)
＝⟨ ap (_∙ rinv (f y)) (ap (ap f) (assocId _ _ _)) ⟩
ap f (ap g p ∙ (linv y ∙ sym (linv y))) ∙ rinv (f y)
＝⟨ ap (_∙ rinv (f y)) (ap (ap f) (relimId _ _ (rinvId _))) ⟩
ap f (ap g p) ∙ rinv (f y)
＝⟨ ap (_∙ rinv (f y)) (apAp _ _ _) ⟩
ap (f ∘ g) p ∙ rinv (f y)
＝⟨ sym (naturalityHtpy rinv p) ⟩
rinv (f x) ∙ ap (idFunction _) p
＝⟨ ap (rinv (f x) ∙_) (apId p) ⟩
rinv (f x) ∙ p
∎
zz : ∀ (p : f x ＝ f y) → ap f (sym (linv x) ∙ (ap g p ∙ linv y)) ＝ p
zz p = lcancelId (rinv (f x)) _ p (zy p)