# Pointed families of types

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

Created on 2022-05-07.

module structured-types.pointed-families-of-types where

Imports
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import structured-types.pointed-types


## Idea

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.

## Definition

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)
where

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


## Examples

### The constant pointed family

module _
{l1 l2 : Level}
where

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)