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. Those are called pointed maps.

_β†’βˆ™_ : Typeβˆ™ β„“ β†’ Typeβˆ™ β„“' β†’ Type _
(A , a) β†’βˆ™ (B , b) = Ξ£[ f ∈ (A β†’ B) ] (f a ≑ b)

Pointed maps compose in a straightforward way.

idβˆ™ : A β†’βˆ™ A
idβˆ™ = id , refl

_βˆ˜βˆ™_ : (B β†’βˆ™ C) β†’ (A β†’βˆ™ B) β†’ A β†’βˆ™ C
(f , ptf) βˆ˜βˆ™ (g , ptg) = f ∘ g , ap f ptg βˆ™ ptf

infixr 40 _βˆ˜βˆ™_

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