Home

同一視型はレトラクトを保存する

module foundations.identity-type-respects-retract where
Imports 
open import foundations.universe
open import foundations.identity-type
open import foundations.sigma-type
open import foundations.retraction
open import foundations.functions-are-functors
open import foundations.groupoid-laws

private variable
  ℓ : Level
  A B : Type ℓ

idRespRetract : ∀ (s : A → B) → HasRetraction s
  → ∀ (x y : A) → HasRetraction (λ (p : x ＝ y) → ap s p)
idRespRetract s (r , rs＝id) x y =
  (λ p → sym (rs＝id x) ∙ (ap r p ∙ rs＝id y)) ,
  λ {refl → ap (sym (rs＝id x) ∙_) (lunitId _) ∙ linvId _}

idResp◅ : (R : A ◅ B)
  → ∀ (x y : A) → Id A x y ◅ Id B (R .fst x) (R .fst y)
idResp◅ (s , hasR) x y = ap s , idRespRetract s hasR x y