Precomposition of type families

Content created by Egbert Rijke, Fredrik Bakke, Raymond Baker and Vojtěch Štěpančík.

Created on 2023-12-05.
Last modified on 2024-02-06.

module foundation.precomposition-type-families where
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


Any map f : A → B induces a precomposition operation

  (B → 𝒰) → (A → 𝒰)

given by precomposing any Q : B → 𝒰 to Q ∘ f : A → 𝒰.


The precomposition operation on type familes

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B)

  precomp-family : {l : Level}  (B  UU l)  (A  UU l)
  precomp-family Q = Q  f


Transport along homotopies in precomposed type families

Transporting along a homotopy H : g ~ h in the family Q ∘ f gives us a map of families of elements

  ((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.

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}

  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)

    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 
    compute-tr-htpy-precomp-family =
      compute-ind-htpy g
        ( λ h  statement-tr-htpy-precomp-family)
        ( refl-htpy)

Recent changes