Postcomposition of pointed maps

Content created by Egbert Rijke.

Created on 2024-03-13.
Last modified on 2024-03-13.

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

Recent changes