Precomposition of dependent functions

Content created by Egbert Rijke.

Created on 2023-11-24.
Last modified 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)

Recent changes