# Precomposition of dependent functions

Content created by Egbert Rijke.

Created on 2023-11-24.

module foundation-core.precomposition-dependent-functions where

Imports
open import foundation.action-on-identifications-dependent-functions
open import foundation.dependent-homotopies
open import foundation.universe-levels

open import foundation-core.homotopies


## Idea

Given a function f : A → B and a type family X over B, the precomposition function

  - ∘ f : ((y : B) → X b) → ((x : A) → X (f x))


is defined by λ h x → h (f x).

## Definitions

### The precomposition operation on dependent function

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B) (C : B → UU l3)
where

precomp-Π : ((b : B) → C b) → ((a : A) → C (f a))
precomp-Π h a = h (f a)


## Properties

### The action of dependent precomposition on homotopies

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
{f g : A → B} (H : f ~ g) (C : B → UU l3) (h : (y : B) → C y)
where

htpy-precomp-Π :
dependent-homotopy (λ _ → C) H (precomp-Π f C h) (precomp-Π g C h)
htpy-precomp-Π x = apd h (H x)