Action on equivalences of functions

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-09-11.
Last modified on 2023-09-15.

module foundation.action-on-equivalences-functions where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalence-induction
open import foundation.univalence
open import foundation.universe-levels

open import foundation-core.constant-maps
open import foundation-core.contractible-types
open import foundation-core.equivalences
open import foundation-core.identity-types

Idea

Applying the action on identifications to identifications arising from the univalence axiom gives us the action on equivalences.

Alternatively, one can apply transport along identifications to get transport along equivalences, but luckily, these two notions coincide.

Definition

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

  abstract
    unique-action-equiv-function :
      (X : UU l1) →
      is-contr
        ( Σ ((Y : UU l1) → X ≃ Y → f X ＝ f Y) (λ h → h X id-equiv ＝ refl))
    unique-action-equiv-function X =
      is-contr-map-ev-id-equiv
        ( λ Y e → f X ＝ f Y)
        ( refl)

  action-equiv-function :
    {X Y : UU l1} → X ≃ Y → f X ＝ f Y
  action-equiv-function {X} {Y} e = ap f (eq-equiv X Y e)

  compute-action-equiv-function-id-equiv :
    (X : UU l1) → action-equiv-function id-equiv ＝ refl
  compute-action-equiv-function-id-equiv X =
    ap (ap f) (compute-eq-equiv-id-equiv X)

Properties

The action on equivalences of a constant map is constant

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

The action on equivalences of any map preserves composition of equivalences

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

The action on equivalences of any map preserves inverses

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

Recent changes