module 1Lab.Type.Pointed where

Pointed typesπŸ”—

A pointed type is a type AA equipped with a choice of base point βˆ™A\bullet_{A}.

Typeβˆ™ : βˆ€ β„“ β†’ Type (lsuc β„“)
Typeβˆ™ β„“ = Ξ£ (Type β„“) (Ξ» A β†’ A)

If we have pointed types (A,a)(A, a) and (B,b)(B, b), the most natural notion of function between them is not simply the type of functions Aβ†’BA \to B, but rather those functions Aβ†’BA \to B which preserve the basepoint, i.e.Β the functions f:Aβ†’Bf : A \to B equipped with paths f(a)≑bf(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