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* }
Maps∙ : Type∙ ℓ → Type∙ ℓ' → Type∙ (ℓ ⊔ ℓ') Maps∙ A B .fst = A →∙ B Maps∙ A B .snd = zero∙ infixr 0 _→∙_ infixr 40 _∘∙_
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
module _ {ℓ ℓ'} {A@(_ , a₀) : Type∙ ℓ} {B@(_ , b₀) : Type∙ ℓ'} {f∙@(f , φ) g∙@(g , γ) : A →∙ B} where
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₀ ∎
from∙ : B →∙ A from∙ = inverse .fst .fst , inverse .snd id≃∙ : ∀ {ℓ} {A : Type∙ ℓ} → A ≃∙ A id≃∙ = id≃ , refl ≃∙⟨⟩-syntax : ∀ {ℓ ℓ₁ ℓ₂} (A : Type∙ ℓ) {B : Type∙ ℓ₁} {C : Type∙ ℓ₂} → B ≃∙ C → A ≃∙ B → A ≃∙ C ≃∙⟨⟩-syntax A (g , pt) (f , pt') = f ∙e g , ap (g .fst) pt' ∙ pt _≃∙˘⟨_⟩_ : ∀ {ℓ ℓ₁ ℓ₂} (A : Type∙ ℓ) {B : Type∙ ℓ₁} {C : Type∙ ℓ₂} → B ≃∙ A → B ≃∙ C → A ≃∙ C A ≃∙˘⟨ f ⟩≃∙˘ g = ≃∙⟨⟩-syntax _ g (Equiv∙.inverse f) _≃∙⟨⟩_ : ∀ {ℓ ℓ₁} (A : Type∙ ℓ) {B : Type∙ ℓ₁} → A ≃∙ B → A ≃∙ B x ≃∙⟨⟩ x≡y = x≡y _≃∙∎ : ∀ {ℓ} (A : Type∙ ℓ) → A ≃∙ A x ≃∙∎ = id≃∙ infixr 2 ≃∙⟨⟩-syntax _≃∙⟨⟩_ _≃∙˘⟨_⟩_ infix 3 _≃∙∎ infix 21 _≃∙_ syntax ≃∙⟨⟩-syntax x q p = x ≃∙⟨ p ⟩ q path→equiv∙ : A ≡ B → A ≃∙ B path→equiv∙ p .fst = path→equiv (ap fst p) path→equiv∙ p .snd = from-pathp (ap snd p) ua∙-id-equiv : ua∙ {A = A} id≃∙ ≡ refl ua∙-id-equiv {A = A , a₀} i j .fst = ua-id-equiv {A = A} i j ua∙-id-equiv {A = A , a₀} i j .snd = attach (∂ j ∨ i) (λ { (j = i0) → a₀ ; (j = i1) → a₀ ; (i = i1) → a₀ }) (inS 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