Home

h-levelはレトラクトで閉じている

module foundations.h-level-closed-under-retract where
Imports 
open import foundations.universe
open import foundations.h-level
open import foundations.retraction
open import foundations.proposition
open import foundations.set
open import foundations.contractible-type
open import foundations.sigma-type
open import foundations.identity-type
open import foundations.functions-are-functors
open import foundations.groupoid-laws
open import foundations.natural-number
open import foundations.identity-type-respects-retract

private variable
  ℓ : Level
  A B : Type ℓ

isContrRetract : isContr B → A ◅ B → isContr A
isContrRetract (c , f) (s , (r , rs＝id)) = r c , λ a → h a ∙ rs＝id a
  where
    h : ∀ a → r c ＝ r (s a)
    h a = ap r (f (s a))

isPropRetract : isProp B → A ◅ B → isProp A
isPropRetract f (s , (r , rs＝id)) x y = sym (rs＝id x) ∙ (k ∙ rs＝id y)
  where
    k : r (s x) ＝ r (s y)
    k = ap r (f (s x) (s y))

ofHLevelRetract : ∀ n → ofHLevel n B → A ◅ B → ofHLevel n A
ofHLevelRetract zero f r = isContrRetract f r
ofHLevelRetract (suc zero) f r = isPropRetract f r
ofHLevelRetract (suc (suc n)) f (s , hasR) x y =
  ofHLevelRetract (suc n) (f (s x) (s y)) (idResp◅ (s , hasR) x y)

isSetRetract : isSet B → A ◅ B → isSet A
isSetRetract = ofHLevelRetract 2