# 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

Imports
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


## Idea

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.

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


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