{-# OPTIONS --cubical --safe #-} module Cubical.Foundations.Pointed.Properties where open import Cubical.Foundations.Prelude open import Cubical.Foundations.Pointed.Base open import Cubical.Data.Prod Π∙ : ∀ {ℓ ℓ'} (A : Type ℓ) (B∙ : A → Pointed ℓ') → Pointed (ℓ-max ℓ ℓ') Π∙ A B∙ = (∀ a → typ (B∙ a)) , (λ a → pt (B∙ a)) Σ∙ : ∀ {ℓ ℓ'} (A∙ : Pointed ℓ) (B∙ : typ A∙ → Pointed ℓ') → Pointed (ℓ-max ℓ ℓ') Σ∙ A∙ B∙ = (Σ[ a ∈ typ A∙ ] typ (B∙ a)) , (pt A∙ , pt (B∙ (pt A∙))) _×∙_ : ∀ {ℓ ℓ'} (A∙ : Pointed ℓ) (B∙ : Pointed ℓ') → Pointed (ℓ-max ℓ ℓ') A∙ ×∙ B∙ = ((typ A∙) × (typ B∙)) , (pt A∙ , pt B∙)