Transport along identifications
Content created by Egbert Rijke, Fredrik Bakke and Raymond Baker.
Created on 2023-09-11.
Last modified on 2023-11-24.
module foundation.transport-along-identifications where open import foundation-core.transport-along-identifications public
Imports
open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.universe-levels open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types
Idea
Given a type family B
over A
, an
identification p : x = y
in A
and an
element b : B x
, we can
transport the element
b
along the identification p
to obtain an element tr B p b : B y
.
The fact that tr B p
is an equivalence is
recorded in this file.
Properties
Transport is an equivalence
module _ {l1 l2 : Level} {A : UU l1} (B : A → UU l2) {x y : A} where inv-tr : x = y → B y → B x inv-tr p = tr B (inv p) is-retraction-inv-tr : (p : x = y) → (inv-tr p ∘ tr B p) ~ id is-retraction-inv-tr refl b = refl is-section-inv-tr : (p : x = y) → (tr B p ∘ inv-tr p) ~ id is-section-inv-tr refl b = refl is-equiv-tr : (p : x = y) → is-equiv (tr B p) is-equiv-tr p = is-equiv-is-invertible ( inv-tr p) ( is-section-inv-tr p) ( is-retraction-inv-tr p) equiv-tr : x = y → (B x) ≃ (B y) pr1 (equiv-tr p) = tr B p pr2 (equiv-tr p) = is-equiv-tr p
Transporting along refl
is the identity equivalence
equiv-tr-refl : {l1 l2 : Level} {A : UU l1} (B : A → UU l2) {x : A} → equiv-tr B refl = id-equiv {A = B x} equiv-tr-refl B = refl
Computing transport of loops
tr-loop : {l1 : Level} {A : UU l1} {a0 a1 : A} (p : a0 = a1) (l : a0 = a0) → (tr (λ y → y = y) p l) = ((inv p ∙ l) ∙ p) tr-loop refl l = inv right-unit
Recent changes
- 2023-11-24. Egbert Rijke. Refactor precomposition (#937).
- 2023-11-01. Fredrik Bakke. Opposite categories, gaunt categories, replete subprecategories, large Yoneda, and miscellaneous additions (#880).
- 2023-10-22. Egbert Rijke and Fredrik Bakke. Refactor synthetic homotopy theory (#654).
- 2023-09-28. Egbert Rijke and Fredrik Bakke. The Regensburg extension of the fundamental theorem (#803).
- 2023-09-28. Egbert Rijke and Fredrik Bakke. Cyclic types (#800).