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
- 2023-09-15. Fredrik Bakke. Define representations of monoids (#765).
- 2023-09-12. Egbert Rijke. Beyond foundation (#751).
- 2023-09-11. Fredrik Bakke. Transport along and action on equivalences (#706).