Commuting squares of pointed maps
Content created by Fredrik Bakke.
Created on 2023-05-03.
Last modified on 2023-06-08.
module structured-types.commuting-squares-of-pointed-maps where
Imports
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 coherence square of pointed maps
A ------> X
| |
| |
| |
V V
B ------> Y
is a coherence of the underlying square of (unpointed) maps, plus a coherence between the pointedness preservation proofs.
Definition
coherence-square-pointed-maps : {l1 l2 l3 l4 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} {C : Pointed-Type l3} {X : Pointed-Type l4} (top : C →∗ B) (left : C →∗ A) (right : B →∗ X) (bottom : A →∗ X) → UU (l3 ⊔ l4) coherence-square-pointed-maps top left right bottom = (bottom ∘∗ left) ~∗ (right ∘∗ top)
Recent changes
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-05-16. Fredrik Bakke. Swap from
md
totext
code blocks (#622). - 2023-05-03. Fredrik Bakke. Define the smash product of pointed types and refactor pointed types (#583).