module 1Lab.Type.Pointed where

Pointed typesπŸ”—

A pointed type is a type equipped with a choice of base point 

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

If we have pointed types and the most natural notion of function between them is not simply the type of functions but rather those functions which preserve the basepoint, i.e.Β the functions equipped with paths 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