Pointed families of types

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-05-07.
Last modified on 2023-05-03.

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

open import structured-types.pointed-types


A pointed family of types over a pointed type A is a family of types B over the underlying type of A equipped with a base point over the base point of A. Note that a pointed family of types should not be confused with a family of pointed types over A.


Pointed-Fam :
  {l1 : Level} (l : Level) (A : Pointed-Type l1)  UU (lsuc l  l1)
Pointed-Fam l A =
  Σ (type-Pointed-Type A  UU l)  P  P (point-Pointed-Type A))

module _
  {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Fam l2 A)

  fam-Pointed-Fam : type-Pointed-Type A  UU l2
  fam-Pointed-Fam = pr1 B

  point-Pointed-Fam : fam-Pointed-Fam (point-Pointed-Type A)
  point-Pointed-Fam = pr2 B


The constant pointed family

module _
  {l1 l2 : Level}

  constant-Pointed-Fam :
    (A : Pointed-Type l1)  Pointed-Type l2  Pointed-Fam l2 A
  constant-Pointed-Fam A B =
    pair  _  type-Pointed-Type B) (point-Pointed-Type B)

Recent changes