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)


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