# Precomposition of pointed maps

```agda
module structured-types.precomposition-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 "precomposition operation" Disambiguation="pointed maps" Agda=precomp-pointed-map}}
on [pointed maps](structured-types.pointed-maps.md) by a pointed map
`f : A →∗ B` is a family of operations

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

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

## Definitions

### Precomposition by pointed maps

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