Pointed sections of pointed maps
Content created by Jonathan Prieto-Cubides, Fredrik Bakke and Egbert Rijke.
Created on 2022-08-12.
Last modified on 2023-05-03.
module structured-types.pointed-sections where
Imports
open import foundation.dependent-pair-types open import foundation.universe-levels open import structured-types.pointed-homotopies open import structured-types.pointed-maps open import structured-types.pointed-types
Idea
A pointed section of a pointed map f : A →∗ B
consists of a pointed map
g : B →∗ A
equipped with a pointed homotopy H : (f ∘∗ g) ~∗ id
.
pointed-section-Pointed-Type : {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2) → (A →∗ B) → UU (l1 ⊔ l2) pointed-section-Pointed-Type A B f = Σ ( B →∗ A) ( λ g → (f ∘∗ g) ~∗ id-pointed-map)
Recent changes
- 2023-05-03. Fredrik Bakke. Define the smash product of pointed types and refactor pointed types (#583).
- 2023-04-28. Fredrik Bakke. Miscellaneous refactoring and small additions (#579).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).