open import 1Lab.Path
open import 1Lab.Type

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)

private variable
  β„“ β„“' : Level
  A B C : Typeβˆ™ β„“

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)

infixr 0 _β†’βˆ™_

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

The product of two pointed types is again a pointed type.

_Γ—βˆ™_ : Typeβˆ™ β„“ β†’ Typeβˆ™ β„“' β†’ Typeβˆ™ (β„“ βŠ” β„“')
(A , a) Γ—βˆ™ (B , b) = A Γ— B , a , b

infixr 5 _Γ—βˆ™_

fstβˆ™ : A Γ—βˆ™ B β†’βˆ™ A
fstβˆ™ = fst , refl

sndβˆ™ : A Γ—βˆ™ B β†’βˆ™ B
sndβˆ™ = snd , refl