# Postcomposition of pointed maps

```agda
module structured-types.postcomposition-pointed-maps where
```

<details><summary>Imports</summary>

```agda
open import foundation.universe-levels

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

</details>

## Idea

The
{{#concept "postcomposition operation" Disambiguation="pointed maps" Agda=postcomp-pointed-map}}
on [pointed maps](structured-types.pointed-maps.md) by a pointed map
`f : A →∗ B` is a family of operations

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

indexed by a [pointed type](structured-types.pointed-types.md) `X`.

## Definitions

### Postcomposition by pointed maps

```agda
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
```