Home

1以上のh-levelは同一視型のレトラクトで閉じている

module foundations.h-level-closed-under-retract-of-identity 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.homotopy
open import foundations.function
open import foundations.functions-are-functors
open import foundations.groupoid-laws
open import foundations.natural-number
open import foundations.h-level-closed-under-retract

少し面白いことに、isPropRetractIdはHasRetractionを仮定しない。

private variable
  ℓ : Level
  A B : Type ℓ

isPropRetractId : isProp B
  → (s : A → B)
  → (∀ {x y : A} → s x ＝ s y → x ＝ y)
  → isProp A
isPropRetractId f s R x y = R p
  where
    p : s x ＝ s y
    p = f (s x) (s y)

ofHLevelRetractId : ∀ n
  → ofHLevel (suc n) B
  → (s : A → B)
  → (∀ {x y : A} → HasRetraction (ap s {x = x} {y = y}))
  → ofHLevel (suc n) A
ofHLevelRetractId zero f s R = isPropRetractId f s (R .fst)
ofHLevelRetractId {A = A} (suc n) f s R = k
  where
    k : ∀ (x y : A) → ofHLevel (suc n) (x ＝ y)
    k x y = ofHLevelRetract (suc n) (f (s x) (s y)) (ap s , R)

isSetRetractId : isSet B
  → (s : A → B)
  → (∀ {x y : A} → HasRetraction (ap s {x = x} {y = y}))
  → isSet A
isSetRetractId = ofHLevelRetractId 1