{-# 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∙)