The action on identifications of functions
Content created by Egbert Rijke and Fredrik Bakke.
Created on 2023-06-10.
Last modified on 2023-09-11.
module foundation.action-on-identifications-functions where
Imports
open import foundation.universe-levels open import foundation-core.constant-maps open import foundation-core.function-types open import foundation-core.identity-types open import foundation-core.transport-along-identifications
Idea
Any function f : A → B
preserves
identifications, in the sense that it maps
identifications p : x = y
in A
to an identification ap f p : f x = f y
in B
. This action on identifications can be thought of as the functoriality of
identity types.
Definition
The functorial action of functions on identity types
ap : {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) {x y : A} → x = y → (f x) = (f y) ap f refl = refl
Properties
The identity function acts trivially on identifications
ap-id : {l : Level} {A : UU l} {x y : A} (p : x = y) → (ap id p) = p ap-id refl = refl
The action on identifications of a composite function is the composite of the actions
ap-comp : {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} (g : B → C) (f : A → B) {x y : A} (p : x = y) → (ap (g ∘ f) p) = ((ap g ∘ ap f) p) ap-comp g f refl = refl
The action on identifications of any map preserves refl
ap-refl : {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (x : A) → (ap f (refl {x = x})) = refl ap-refl f x = refl
The action on identifications of any map preserves concatenation of identifications
ap-concat : {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) {x y z : A} (p : x = y) (q : y = z) → (ap f (p ∙ q)) = ((ap f p) ∙ (ap f q)) ap-concat f refl q = refl ap-concat-eq : {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) {x y z : A} (p : x = y) (q : y = z) (r : x = z) (H : r = (p ∙ q)) → (ap f r) = ((ap f p) ∙ (ap f q)) ap-concat-eq f p q .(p ∙ q) refl = ap-concat f p q
The action on identifications of any map preserves inverses
ap-inv : {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) {x y : A} (p : x = y) → ap f (inv p) = inv (ap f p) ap-inv f refl = refl
The action on identifications of a constant map is constant
ap-const : {l1 l2 : Level} {A : UU l1} {B : UU l2} (b : B) {x y : A} (p : x = y) → (ap (const A B b) p) = refl ap-const b refl = refl
Transporting along the action on identifications of a function
tr-ap : {l1 l2 l3 l4 : Level} {A : UU l1} {B : A → UU l2} {C : UU l3} {D : C → UU l4} (f : A → C) (g : (x : A) → B x → D (f x)) {x y : A} (p : x = y) (z : B x) → tr D (ap f p) (g x z) = g y (tr B p z) tr-ap f g refl z = refl
The action on identifications of concatenating by refl
on the right
Note that _∙ refl
is only homotopic to the identity function. Therefore we
will compute here the action on identifications of the map _∙ refl
.
inv-ap-refl-concat : {l : Level} {A : UU l} {x y : A} {p q : x = y} (r : p = q) → (right-unit ∙ (r ∙ inv right-unit)) = (ap (_∙ refl) r) inv-ap-refl-concat refl = right-inv right-unit ap-refl-concat : {l : Level} {A : UU l} {x y : A} {p q : x = y} (r : p = q) → (ap (_∙ refl) r) = (right-unit ∙ (r ∙ inv right-unit)) ap-refl-concat = inv ∘ inv-ap-refl-concat
Recent changes
- 2023-09-11. Fredrik Bakke. Transport along and action on equivalences (#706).
- 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).