# Precomposition of type families

```agda
module foundation.precomposition-type-families where
```

<details><summary>Imports</summary>

```agda
open import foundation.homotopy-induction
open import foundation.transport-along-homotopies
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types
```

</details>

## Idea

Any map `f : A โ†’ B` induces a
{{#concept "precomposition operation" Disambiguation="type families" Agda=precomp-family}}

```text
  (B โ†’ ๐’ฐ) โ†’ (A โ†’ ๐’ฐ)
```

given by [precomposing](foundation-core.precomposition-functions.md) any
`Q : B โ†’ ๐’ฐ` to `Q โˆ˜ f : A โ†’ ๐’ฐ`.

## Definitions

### The precomposition operation on type familes

```agda
module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A โ†’ B)
  where

  precomp-family : {l : Level} โ†’ (B โ†’ UU l) โ†’ (A โ†’ UU l)
  precomp-family Q = Q โˆ˜ f
```

## Properties

### Transport along homotopies in precomposed type families

[Transporting](foundation.transport-along-homotopies.md) along a
[homotopy](foundation.homotopies.md) `H : g ~ h` in the family `Q โˆ˜ f` gives us
a map of families of elements

```text
  ((a : A) โ†’ Q (f (g a))) โ†’ ((a : A) โ†’ Q (f (h a))) .
```

We show that this map is homotopic to transporting along
`f ยทl H : f โˆ˜ g ~ f โˆ˜ h` in the family `Q`.

```agda
module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} (f : A โ†’ B) (Q : B โ†’ UU l3)
  {X : UU l4} {g : X โ†’ A}
  where

  statement-tr-htpy-precomp-family :
    {h : X โ†’ A} (H : g ~ h) โ†’ UU (l3 โŠ” l4)
  statement-tr-htpy-precomp-family H =
    tr-htpy (ฮป _ โ†’ precomp-family f Q) H ~ tr-htpy (ฮป _ โ†’ Q) (f ยทl H)

  abstract
    tr-htpy-precomp-family :
      {h : X โ†’ A} (H : g ~ h) โ†’
      statement-tr-htpy-precomp-family H
    tr-htpy-precomp-family =
      ind-htpy g
        ( ฮป h โ†’ statement-tr-htpy-precomp-family)
        ( refl-htpy)

    compute-tr-htpy-precomp-family :
      tr-htpy-precomp-family refl-htpy ๏ผ
      refl-htpy
    compute-tr-htpy-precomp-family =
      compute-ind-htpy g
        ( ฮป h โ†’ statement-tr-htpy-precomp-family)
        ( refl-htpy)
```