Action on equivalences of functions

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-09-11.
Last modified on 2024-04-11.

module foundation.action-on-equivalences-functions where
open import foundation.action-on-higher-identifications-functions
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


Given a map between universes f : 𝒰 → 𝒱, then applying the action on identifications to identifications arising from the univalence axiom gives us the action on equivalences

  action-equiv-function f : X ≃ Y → f X ≃ f Y.

Alternatively, one can apply transport along identifications to get transport along equivalences. However, by univalence such an action must also be unique, hence these two constructions coincide.


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

    unique-action-equiv-function :
      (X : UU l1) 
        ( Σ ((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 e = ap f (eq-equiv e)

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


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) e)  refl
compute-action-equiv-function-const b e = ap-const b (eq-equiv 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 e e' =
    ( ap² f (inv (compute-eq-equiv-comp-equiv e e'))) 
    ( ap-concat f (eq-equiv e) (eq-equiv 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 e =
  ( ap² f (inv (commutativity-inv-eq-equiv e))) 
  ( ap-inv f (eq-equiv e))

Recent changes