# The action on equivalences of functions out of subuniverses

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-09-12.

module foundation.action-on-equivalences-functions-out-of-subuniverses 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.subuniverses
open import foundation.universe-levels

open import foundation-core.contractible-types
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.identity-types


## Idea

Consider a subuniverse P of 𝒰 and a map f : P → B from the subuniverse P into some type B. Then f has an action on equivalences

  (X ≃ Y) → (f X ＝ f Y)


which is uniquely determined by the identification action-equiv f id-equiv ＝ refl. The action on equivalences fits in a commuting square of maps

                     ap f
(X = Y) ---------------> (f X = f Y)
|                          |
equiv-eq |                          | id
∨                          ∨
(X ≃ Y) ---------------> (f X = f Y)
action-equiv f


## Definitions

module _
{l1 l2 l3 : Level} (P : subuniverse l1 l2)
{B : UU l3} (f : type-subuniverse P → B)
where

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

action-equiv-function-subuniverse :
(X Y : type-subuniverse P) → equiv-subuniverse P X Y → f X ＝ f Y
action-equiv-function-subuniverse X Y =
ap f ∘ eq-equiv-subuniverse P

compute-action-equiv-function-subuniverse-id-equiv :
(X : type-subuniverse P) →
action-equiv-function-subuniverse X X id-equiv ＝ refl
compute-action-equiv-function-subuniverse-id-equiv X =
ap² f (compute-eq-equiv-id-equiv-subuniverse P)