module 1Lab.Type.Pointed where

## Pointed typesπ

A **pointed type** is a type
$A$
equipped with a choice of base point
$\bullet_{A}$.

Typeβ : β β β Type (lsuc β) Typeβ β = Ξ£ (Type β) (Ξ» A β A)

If we have pointed types
$(A, a)$
and
$(B, b)$,
the most natural notion of function between them is not simply the type
of functions
$A \to B$,
but rather those functions
$A \to B$
which *preserve the basepoint*, i.e.Β the functions
$f : A \to B$
equipped with paths
$f(a) \equiv b$.

_ββ_ : Typeβ β β Typeβ ββ² β Type _ (A , a) ββ (B , b) = Ξ£[ f β (A β B) ] (f a β‘ b)

Paths between pointed maps are characterised as **pointed
homotopies**:

funextβ : {f g : A ββ B} β (h : β x β f .fst x β‘ g .fst x) β Square (h (A .snd)) (f .snd) (g .snd) refl β f β‘ g funextβ h pth i = funext h i , pth i