Pointed dependent pair types

Content created by Fredrik Bakke.

Created on 2023-04-28.
Last modified on 2025-10-31.

module structured-types.pointed-dependent-pair-types where
Imports 
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import structured-types.pointed-families-of-types
open import structured-types.pointed-types

Idea

Given a pointed type (A , a) and a pointed family over it (B , b), then we may form the pointed dependent pair type Σ A B, which is canonically pointed at (a , b).

Definition

module _
  {l1 l2 : Level}
  where

  Σ-Pointed-Type :
    (A : Pointed-Type l1) → Pointed-Fam l2 A → Pointed-Type (l1 ⊔ l2)
  Σ-Pointed-Type (A , a) (B , b) = (Σ A B , (a , b))

  Σ∗ : (A : Pointed-Type l1) → Pointed-Fam l2 A → Pointed-Type (l1 ⊔ l2)
  Σ∗ = Σ-Pointed-Type

Note: the subscript asterisk symbol used for the pointed dependent pair type Σ∗, and pointed type constructions in general, is the asterisk operator ∗ (agda-input: \ast), not the asterisk *.

Recent changes