Action on equivalences of type families

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-09-12.
Last modified on 2024-04-25.

module foundation.action-on-equivalences-type-families where
Imports 
open import foundation.action-on-equivalences-functions
open import foundation.action-on-identifications-functions
open import foundation.equivalence-induction
open import foundation.univalence
open import foundation.universe-levels
open import foundation.whiskering-higher-homotopies-composition

open import foundation-core.commuting-squares-of-maps
open import foundation-core.constant-maps
open import foundation-core.contractible-types
open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types

Ideas

Any family of types B : 𝒰 → 𝒱 over a universe 𝒰 has an action on equivalences

  (A ≃ B) → P A ≃ P B

obtained by equivalence induction. The acion on equivalences of a type family B on a universe 𝒰 is uniquely determined by the identification B id-equiv ＝ id-equiv, and fits in a commuting square

                   ap B
        (X ＝ Y) --------> (B X ＝ B Y)
           |                    |
  equiv-eq |                    | equiv-eq
           ∨                    ∨
        (X ≃ Y) ---------> (B X ≃ B Y).
                     B

Note: In general -- in particular in our general constructions below -- we need the univalence axiom to construct the action on equivalences of a family of types. However, for many specific type families that are defined in terms of the basic type constructors, we can construct the action on equivalences directly without invoking the univalence axiom.

Definitions

The action on equivalences of a family of types over a universe

module _
  {l1 l2 : Level} (B : UU l1 → UU l2)
  where

  abstract
    unique-action-equiv-family :
      {X : UU l1} →
      is-contr (fiber (ev-id-equiv (λ Y e → B X ≃ B Y)) id-equiv)
    unique-action-equiv-family =
      is-contr-map-ev-id-equiv (λ Y e → B _ ≃ B Y) id-equiv

  action-equiv-family :
    {X Y : UU l1} → (X ≃ Y) → B X ≃ B Y
  action-equiv-family {X} {Y} =
    equiv-eq ∘ action-equiv-function B

  compute-action-equiv-family-id-equiv :
    {X : UU l1} →
    action-equiv-family {X} {X} id-equiv ＝ id-equiv
  compute-action-equiv-family-id-equiv {X} =
    ap equiv-eq (compute-action-equiv-function-id-equiv B X)

  map-action-equiv-family : {X Y : UU l1} → X ≃ Y → B X → B Y
  map-action-equiv-family = map-equiv ∘ action-equiv-family

Properties

The action on equivalences of a family of types over a universe fits in a commuting square with equiv-eq

We claim that the square

                   ap B
        (X ＝ Y) --------> (B X ＝ B Y)
           |                    |
  equiv-eq |                    | equiv-eq
           ∨                    ∨
        (X ≃ Y) ---------> (B X ≃ B Y).
                     B

commutes for any two types X Y : 𝒰 and any type family B over 𝒰.

coherence-square-action-equiv-family :
  {l1 l2 : Level} (B : UU l1 → UU l2) (X Y : UU l1) →
  coherence-square-maps
    ( ap B {X} {Y})
    ( equiv-eq)
    ( equiv-eq)
    ( action-equiv-family B)
coherence-square-action-equiv-family B X .X refl =
  compute-action-equiv-family-id-equiv B

The identity function acts trivially on equivalences

compute-action-equiv-family-id :
  {l : Level} {X Y : UU l} (e : X ≃ Y) → (action-equiv-family id e) ＝ e
compute-action-equiv-family-id e =
  ap equiv-eq (ap-id (eq-equiv e)) ∙ is-section-eq-equiv e

The action on equivalences of a constant map is constant

compute-action-equiv-family-const :
  {l1 l2 : Level} (B : UU l2) {X Y : UU l1}
  (e : X ≃ Y) → (action-equiv-family (const (UU l1) B) e) ＝ id-equiv
compute-action-equiv-family-const B {X} {Y} e =
  ap equiv-eq (compute-action-equiv-function-const B e)

The action on equivalences of a composite function is the composite of the actions

distributive-action-equiv-function-comp :
  {l1 l2 l3 : Level} {C : UU l3} (g : UU l2 → C) (f : UU l1 → UU l2)
  {X Y : UU l1} →
  action-equiv-function (g ∘ f) {X} {Y} ~
  action-equiv-function g ∘ action-equiv-family f
distributive-action-equiv-function-comp g f e =
  ( ap-comp g f (eq-equiv e)) ∙
  ( left-whisker-comp² g
    ( inv-htpy is-retraction-eq-equiv)
    ( action-equiv-function f e))

distributive-action-equiv-family-comp :
  {l1 l2 l3 : Level} (g : UU l2 → UU l3) (f : UU l1 → UU l2)
  {X Y : UU l1} →
  action-equiv-family (g ∘ f) {X} {Y} ~
  action-equiv-family g ∘ action-equiv-family f
distributive-action-equiv-family-comp g f e =
  ap equiv-eq (distributive-action-equiv-function-comp g f e)

The action on equivalences of any map preserves composition of equivalences

distributive-action-equiv-family-comp-equiv :
  {l1 l2 : Level} (f : UU l1 → UU l2) {X Y Z : UU l1} →
  (e : X ≃ Y) (e' : Y ≃ Z) →
  action-equiv-family f (e' ∘e e) ＝
  action-equiv-family f e' ∘e action-equiv-family f e
distributive-action-equiv-family-comp-equiv f e e' =
  ( ap equiv-eq (distributive-action-equiv-function-comp-equiv f e e')) ∙
  ( inv
    ( compute-equiv-eq-concat
      ( action-equiv-function f e)
      ( action-equiv-function f e')))

The action on equivalences of any map preserves inverses

compute-action-equiv-family-inv-equiv :
  {l1 l2 : Level} (f : UU l1 → UU l2) {X Y : UU l1}
  (e : X ≃ Y) →
  action-equiv-family f (inv-equiv e) ＝ inv-equiv (action-equiv-family f e)
compute-action-equiv-family-inv-equiv f e =
  ( ap equiv-eq (compute-action-equiv-function-inv-equiv f e)) ∙
  ( inv (commutativity-inv-equiv-eq (action-equiv-function f e)))

Recent changes