Cavallo's trick
Content created by Egbert Rijke and Fredrik Bakke.
Created on 2023-05-03.
Last modified on 2023-07-19.
module synthetic-homotopy-theory.cavallos-trick where
Imports
open import foundation.action-on-identifications-functions open import foundation.dependent-pair-types open import foundation.function-types open import foundation.homotopies open import foundation.identity-types open import foundation.sections open import foundation.universe-levels open import structured-types.pointed-homotopies open import structured-types.pointed-maps open import structured-types.pointed-types
Idea
Cavallo's trick is a way of upgrading an unpointed homotopy between pointed maps
to a pointed homotopy. Originally, this trick was formulated by Evan Cavallo for
homogeneous spaces, but it works as soon as the evaluation map (id ~ id) → Ω B
has a section.
Theorem
module _ {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} where cavallos-trick : (f g : A →∗ B) → section (λ (H : id ~ id) → H (point-Pointed-Type B)) → (map-pointed-map f ~ map-pointed-map g) → f ~∗ g pr1 (cavallos-trick (f , refl) (g , q) (K , α) H) a = K (inv q ∙ inv (H (point-Pointed-Type A))) (f a) ∙ H a pr2 (cavallos-trick (f , refl) (g , q) (K , α) H) = ( ap ( concat' (f (point-Pointed-Type A)) (H (point-Pointed-Type A))) ( α (inv q ∙ inv (H (point-Pointed-Type A))))) ∙ ( ( assoc ( inv q) ( inv (H (point-Pointed-Type A))) ( H (point-Pointed-Type A))) ∙ ( ( ap ( concat (inv q) (g (point-Pointed-Type A))) ( left-inv (H (point-Pointed-Type A)))) ∙ ( right-unit)))
References
- Cavallo's trick was originally formalized in the cubical agda library.
- The above generalization was found by Buchholtz, Christensen, Rijke, and Taxerås Flaten, in Central H-spaces and banded types
Recent changes
- 2023-07-19. Egbert Rijke. refactoring pointed maps (#682).
- 2023-06-15. Egbert Rijke. Replace
isretr
withis-retraction
andissec
withis-section
(#659). - 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).
- 2023-05-03. Fredrik Bakke. Define the smash product of pointed types and refactor pointed types (#583).