Home

依存積のh-level

module foundations.h-level-pi 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.function-extensionality
open import foundations.identity-type
open import foundations.sigma-type
open import foundations.h-level-closed-under-retract
open import foundations.happly
open import foundations.implicit-function

関数の外延性が必要となる。

private variable
  ℓ ℓ′ ℓ″ : Level

module _ {A : Type ℓ} {B : A → Type ℓ′} (e : FunExtType A B) where
  isContrΠ : (∀ (a : A) → isContr (B a)) → isContr ((a : A) → B a)
  isContrΠ f .fst a = f a .fst
  isContrΠ f .snd g = byFunExtType e _ g λ x → snd (f x) (g x)

  isPropΠ : (∀ (a : A) → isProp (B a)) → isProp ((a : A) → B a)
  isPropΠ f g h = byFunExtType e g h (λ x → f x (g x) (h x))

module _  (e : FunExtLevel ℓ ℓ′) where
  ofHLevelΠ : ∀ {A : Type ℓ} {B : A → Type ℓ′}
    → ∀ n
    → (∀ (a : A) → ofHLevel n (B a))
    → ofHLevel n ((a : A) → B a)
  ofHLevelΠ zero f = isContrΠ e f
  ofHLevelΠ (suc zero) f = isPropΠ e f
  ofHLevelΠ (suc (suc n)) f g h =
    ofHLevelRetract
      (suc n)
      (ofHLevelΠ (suc n) (λ a → f a (g a) (h a)))
      (happly , (byFunExtType e g h , retractByFunExtType e g h))

  isSetΠ : ∀ {A : Type ℓ} {B : A → Type ℓ′} → (∀ (a : A) → isSet (B a)) → isSet ((a : A) → B a)
  isSetΠ = ofHLevelΠ 2

  isSet→ : ∀ {A : Type ℓ} {B : Type ℓ′} → (A → isSet B) → isSet (A → B)
  isSet→ = isSetΠ

いくつか便利関数を定義しておく。

module _ {A : Type ℓ} {B : A → Type ℓ′} (e : FunExtType A B) where
  isPropImplicitΠ : (∀ (a : A) → isProp (B a)) → isProp (∀ {a : A} → B a)
  isPropImplicitΠ f =
    isPropRetract
      (isPropΠ e f)
      (toExplicitΠ , (toImplicitΠ , λ _ → refl))

module _ {A : Type ℓ} {B : A → Type ℓ′} (e : FunExtLevel ℓ ℓ′) where
  ofHLevelImplicitΠ : ∀ n → (∀ (a : A) → ofHLevel n (B a)) → ofHLevel n (∀ {a : A} → B a)
  ofHLevelImplicitΠ n f = ofHLevelRetract n (ofHLevelΠ e n f) (toExplicitΠ , (toImplicitΠ , λ _ → refl))

  isSetImplicitΠ : (∀ (a : A) → isSet (B a)) → isSet (∀ {a : A} → B a)
  isSetImplicitΠ = ofHLevelImplicitΠ 2

module _ {A : Type ℓ} {B : A → Type ℓ} {C : (a : A) → B a → Type ℓ}
  (e : FunExtLevel ℓ ℓ) where
  isPropΠ2 : (∀ (a : A) (b : B a) → isProp (C a b)) → isProp (∀ (a : A) (b : B a) → C a b)
  isPropΠ2 f = isPropΠ e λ a → isPropΠ e (f a)

  isPropImplicitΠ2 : (∀ (a : A) (b : B a) → isProp (C a b)) → isProp (∀ {a : A} {b : B a} → C a b)
  isPropImplicitΠ2 f = isPropImplicitΠ e λ a → isPropImplicitΠ e (f a)