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)

The type of pointed maps is always inhabited by the constant function with value which we refer to as the zero map. This makes the type itself a pointed type; in the code, we write Maps∙. As further examples, the identity is evidently pointed, and the composition of pointed maps is once again pointed.

zero∙ : A →∙ B
zero∙ {B = _ , b₀} = record { snd = refl }

id∙ : A →∙ A
id∙ = id , refl

_∘∙_ : (B →∙ C)  (A →∙ B)  A →∙ C
(f , f*) ∘∙ (g , g*) = record
  { fst = f  g
  ; snd = ap f g*  f*
  }

The product of pointed types is naturally pointed (at the pairing of the basepoints), and this definition makes the fst and snd projections into pointed maps.

_×∙_ : 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

Paths between pointed maps are characterised as pointed homotopies. If we are comparing and as pointed maps it suffices to give a homotopy and a Square with the boundary below. We note in passing that this is equivalent to asking for a proof that

  funext∙ : (h :  x  f x  g x)  Square (h a₀) φ γ refl  f∙  g∙
  funext∙ h pth i = record
    { fst = funext h i
    ; snd = pth i
    }

  _ : (h :  x  f x  g x)  φ  h a₀  γ  f∙  g∙
  _ = λ h α  funext∙ h (flip₁ (∙→square' α))

Pointed equivalences🔗

Combining our univalent understanding of paths in the universe, and our understanding of paths in types, it stands to reason that identifications in the space of pointed types are given by equivalences which carry to We call these a pointed equivalence from to and, as expected, we can directly use cubical primitives to turn a pointed equivalence into a path of pointed types.

_≃∙_ : Type∙   Type∙ ℓ'  Type _
(A , a₀) ≃∙ (B , b₀) = Σ[ e  A  B ] (e · a₀  b₀)

ua∙ : A ≃∙ B  A  B
ua∙ (e , p) i .fst = ua e i
ua∙ (e , p) i .snd = path→ua-pathp e p i

Of course, a pointed equivalence has an underlying pointed map, by simply swapping the quantifiers. Less directly, the inverse of a pointed equivalence is a pointed equivalence as well.

  to∙ : A →∙ B
  to∙ = e .fst .fst , e .snd

  open Equiv (e .fst) hiding (inverse) public

  inverse : B ≃∙ A
  inverse .fst = Equiv.inverse (e .fst)
  inverse .snd = injective $
    e · from b₀ ≡⟨ Equiv.ε (e .fst) _ 
    b₀          ≡˘⟨ e .snd ≡˘
    e · a₀      

Moreover, we can prove that pointed equivalences are an identity system on the type of pointed types, again by a pretty direct cubical argument.

univalence∙-identity-system
  : is-identity-system {A = Type∙ } _≃∙_  _  id≃∙)
univalence∙-identity-system .to-path = ua∙
univalence∙-identity-system .to-path-over {a = A , a₀} (e , e*) i = record
  { fst =
    let
      f :  i  A  ua e i
      f i a = path→ua-pathp e refl i
    in f i , is-prop→pathp  i  is-equiv-is-prop (f i)) id-equiv (e .snd) i
  ; snd = λ j  path→ua-pathp e  k  e* (j  k)) i
  }

Note that this immediately lets us obtain a pointed equivalence induction principle.

Equiv∙J
  :  { ℓ'} {A : Type∙ } (P : (B : Type∙ )  A ≃∙ B  Type ℓ')
   P A id≃∙
    {B} e  P B e
Equiv∙J = IdsJ univalence∙-identity-system

Homogeneity🔗

Coming up with pointed homotopies is tricky when there’s a lot of path algebra involved in showing that the underlying functions are identical, since we would have to trace the pointedness witness along this construction. However, there is a simplifying assumption we can impose on the codomain that makes this much simpler, allowing us to consider only the underlying functions to begin with.

We say that a type is homogeneous if, given two choices of basepoint we have that in the type of pointed types.

Homogeneous : Type   Type _
Homogeneous A =  {x y}  Path (Type∙ _) (A , x) (A , y)

By univalence, this is equivalent to asking for, given an equivalence with This provides us some example that the notion is not vacuous: for example, if we can decide equality in then we can build such an equivalence by case analysis.

Another example is readily given by path spaces, where if we are given then precomposition with is an auto-equivalence of which sends to thence an identification between the pointed types and

instance
  Path-homogeneous :  {} {A : Type } {x y : A}  Homogeneous (Path A x y)
  Path-homogeneous {x = _} {_} {p} {q} = ua∙ record
    { fst = ∙-pre-equiv (q  sym p)
    ; snd = ∙-cancelr q p
    }

If are pointed maps into a homogeneous type then to get an identity it suffices to identify the underlying unpointed maps

homogeneous-funext∙
  :  { ℓ'} {A : Type∙ } {B : Type∙ ℓ'}
    _ : Homogeneous (B .fst) 
    {f g : A →∙ B} (h :  x  f .fst x  g .fst x)
   f  g
homogeneous-funext∙ {A = A} {B = B , b₀} {f = f∙@(f , f*)} {g∙@(g , g*)} h =
  subst  b  PathP  i  A →∙ b i) f∙ g∙) fix bad where
    hom :  x  Path (Type∙ _) (B , b₀) (B , x)
    hom x = auto

    fg* = sym f* ∙∙ h (A .snd) ∙∙ g*

    bad : PathP  i  A →∙ B , fg* i) f∙ g∙
    bad i .fst x = h x i
    bad i .snd j = ∙∙-filler (sym f*) (h (A .snd)) g* j i

    fix : Square {A = Type∙ _} refl  i  B , fg* i) refl refl
    fix i j = hcomp ( i   j) λ where
      k (k = i0)  B , b₀
      k (i = i0)  hom (fg* j) k
      k (i = i1)  hom b₀ k
      k (j = i0)  hom b₀ k
      k (j = i1)  hom b₀ k