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
Imports 
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

Idea

Any map f : A → B induces a precomposition operation

  (B → 𝒰) → (A → 𝒰)

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

Definitions

The precomposition operation on type familes

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 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}
  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)

Recent changes