module foundations.greater-h-levels where
open import foundations.universe open import foundations.natural-number open import foundations.contractible-type open import foundations.proposition open import foundations.identity-type open import foundations.h-level open import foundations.sigma-type open import foundations.groupoid-laws open import foundations.set open import foundations.dependent-map open import foundations.transport open import foundations.transport-identity open import foundations.identity-type-reasoning
まずはbase caseを示す。
private variable
ℓ : Level
A : Type ℓ
isContr⇒isProp : isContr A → isProp A
isContr⇒isProp (a , f) x y = sym (f x) ∙ f y
isProp⇒isSet : isProp A → isSet A
isProp⇒isSet {A = A} f a b q r = toCanonical q ∙ sym (toCanonical r)
where
g : ∀ (y : A) → a ＝ y
g y = f a y
h : ∀ {x y : A} → (p : x ＝ y) → g x ∙ p ＝ g y
h p = sym (substCod p (f a _)) ∙ apd g p
toCanonical : ∀ {x y : A} → (p : x ＝ y) → p ＝ sym (g x) ∙ g y
toCanonical p =
lcancelId (g _) p _ (h p ∙ sym (sym (assocId _ _ _) ∙ lelimId _ _ (rinvId _)))
後は帰納法を使う。
ofHLevelSuc : ∀ n → ofHLevel n A → ofHLevel (suc n) A ofHLevelSuc zero f = isContr⇒isProp f ofHLevelSuc (suc zero) f = isProp⇒isSet f ofHLevelSuc (suc (suc n)) f a b = ofHLevelSuc (suc n) (f a b)