Home

依存和のh-level

module foundations.h-level-sigma where
Imports 
open import foundations.universe
open import foundations.h-level
open import foundations.natural-number
open import foundations.contractible-type
open import foundations.proposition
open import foundations.set
open import foundations.identity-type
open import foundations.sigma-type
open import foundations.sigma-type-identity
open import foundations.h-level-closed-under-retract
open import foundations.greater-h-levels
open import foundations.transport

private variable
  ℓ : Level
  A : Type ℓ
  B : A → Type ℓ

isContrΣ : isContr A → (∀ a → isContr (B a)) → isContr (Σ A B)
isContrΣ (a , f) g .fst = a , g a .fst
isContrΣ (a , f) g .snd (x , y) = toΣId (f x , isContr⇒isProp (g x) _ y)

isPropΣ : isProp A → (∀ a → isProp (B a)) → isProp (Σ A B)
isPropΣ f g (a , b) (a′ , b′) = toΣId (f a a′ , g a′ _ b′)

ofHLevelΣ : ∀ n → ofHLevel n A → (∀ a → ofHLevel n (B a)) → ofHLevel n (Σ A B)
ofHLevelΣ zero f g = isContrΣ f g
ofHLevelΣ (suc zero) f g = isPropΣ f g
ofHLevelΣ {A = A} {B = B} (suc (suc n)) f g (a , b) (a′ , b′) =
  ofHLevelRetract
    (suc n)
    (ofHLevelΣ (suc n) (f a a′) (λ p → g a′ (subst B p b) b′))
    (fromΣId , ΣId .fst)

isSetΣ : isSet A → (∀ a → isSet (B a)) → isSet (Σ A B)
isSetΣ = ofHLevelΣ 2