This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Precomposition of pointed maps

module structured-types.precomposition-pointed-maps where
Imports 
open import foundation.universe-levels

open import structured-types.pointed-maps
open import structured-types.pointed-types

Idea

The precomposition operation on pointed maps by a pointed map f : A →∗ B is a family of operations

  - ∘∗ f : (B →∗ C) → (A →∗ C)

indexed by a pointed type C.

Definitions

Precomposition by pointed maps

precomp-pointed-map :
  {l1 l2 l3 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B)
  (C : Pointed-Type l3) → (B →∗ C) → (A →∗ C)
precomp-pointed-map f C g = comp-pointed-map g f