Join powers of types

Content created by Egbert Rijke.

Created on 2023-06-14.
Last modified on 2023-06-14.

module synthetic-homotopy-theory.join-powers-of-types where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.empty-types
open import foundation.iterating-functions
open import foundation.universe-levels

open import synthetic-homotopy-theory.joins-of-types

Idea

The n-th join power of a type A is defined by taking the n-fold join of A with itself.

Definitions

Join powers of types

join-power : {l1 : Level} → ℕ → UU l1 → UU l1
join-power n A = iterate n (join A) (raise-empty _)

Join powers of type families

join-power-family-of-types :
  {l1 l2 : Level} → ℕ → {A : UU l1} → (A → UU l2) → (A → UU l2)
join-power-family-of-types n B a = join-power n (B a)

Recent changes