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

Postcomposition of pointed maps

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

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

Idea

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

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

indexed by a pointed type X.

Definitions

Postcomposition by pointed maps

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