From aba55fc5d97bf4b227098be635fc4d0f586d7c25 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 28 Nov 2025 15:06:56 +0000 Subject: [PATCH 01/12] terminology change cospans --- src/foundation/cospan-diagrams.lagda.md | 16 ++++++++-------- src/foundation/cospans.lagda.md | 8 ++++---- src/foundation/equivalences-cospans.lagda.md | 4 ++-- .../morphisms-cospan-diagrams.lagda.md | 16 ++++++++-------- src/foundation/morphisms-cospans.lagda.md | 4 ++-- src/foundation/pullback-cones.lagda.md | 4 ++-- ...localizations-at-global-subuniverses.lagda.md | 12 ++++++------ .../reflective-global-subuniverses.lagda.md | 4 ++-- 8 files changed, 34 insertions(+), 34 deletions(-) diff --git a/src/foundation/cospan-diagrams.lagda.md b/src/foundation/cospan-diagrams.lagda.md index 47673304e16..74b1859f133 100644 --- a/src/foundation/cospan-diagrams.lagda.md +++ b/src/foundation/cospan-diagrams.lagda.md @@ -33,25 +33,25 @@ module _ {l1 l2 l3 : Level} (c : cospan-diagram l1 l2 l3) where - left-type-cospan-diagram : UU l1 - left-type-cospan-diagram = pr1 c + domain-cospan-diagram : UU l1 + domain-cospan-diagram = pr1 c - right-type-cospan-diagram : UU l2 - right-type-cospan-diagram = pr1 (pr2 c) + codomain-cospan-diagram : UU l2 + codomain-cospan-diagram = pr1 (pr2 c) cospan-cospan-diagram : - cospan l3 left-type-cospan-diagram right-type-cospan-diagram + cospan l3 domain-cospan-diagram codomain-cospan-diagram cospan-cospan-diagram = pr2 (pr2 c) cospanning-type-cospan-diagram : UU l3 - cospanning-type-cospan-diagram = codomain-cospan cospan-cospan-diagram + cospanning-type-cospan-diagram = cospanning-type-cospan cospan-cospan-diagram left-map-cospan-diagram : - left-type-cospan-diagram → cospanning-type-cospan-diagram + domain-cospan-diagram → cospanning-type-cospan-diagram left-map-cospan-diagram = left-map-cospan cospan-cospan-diagram right-map-cospan-diagram : - right-type-cospan-diagram → cospanning-type-cospan-diagram + codomain-cospan-diagram → cospanning-type-cospan-diagram right-map-cospan-diagram = right-map-cospan cospan-cospan-diagram ``` diff --git a/src/foundation/cospans.lagda.md b/src/foundation/cospans.lagda.md index 41f0b583d6e..bbed314d7ee 100644 --- a/src/foundation/cospans.lagda.md +++ b/src/foundation/cospans.lagda.md @@ -61,13 +61,13 @@ module _ {l1 l2 : Level} {l : Level} {A : UU l1} {B : UU l2} (c : cospan l A B) where - codomain-cospan : UU l - codomain-cospan = pr1 c + cospanning-type-cospan : UU l + cospanning-type-cospan = pr1 c - left-map-cospan : A → codomain-cospan + left-map-cospan : A → cospanning-type-cospan left-map-cospan = pr1 (pr2 c) - right-map-cospan : B → codomain-cospan + right-map-cospan : B → cospanning-type-cospan right-map-cospan = pr2 (pr2 c) ``` diff --git a/src/foundation/equivalences-cospans.lagda.md b/src/foundation/equivalences-cospans.lagda.md index a44b7e3b112..2f2dac5bde8 100644 --- a/src/foundation/equivalences-cospans.lagda.md +++ b/src/foundation/equivalences-cospans.lagda.md @@ -53,7 +53,7 @@ module _ equiv-cospan : cospan l3 A B → cospan l4 A B → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) equiv-cospan c d = - Σ ( codomain-cospan c ≃ codomain-cospan d) + Σ ( cospanning-type-cospan c ≃ cospanning-type-cospan d) ( λ e → coherence-hom-cospan c d (map-equiv e)) ``` @@ -87,7 +87,7 @@ module _ is-torsorial-equiv-cospan c = is-torsorial-Eq-structure ( is-torsorial-equiv (pr1 c)) - ( codomain-cospan c , id-equiv) + ( cospanning-type-cospan c , id-equiv) ( is-torsorial-Eq-structure ( is-torsorial-htpy' (left-map-cospan c)) ( left-map-cospan c , refl-htpy) diff --git a/src/foundation/morphisms-cospan-diagrams.lagda.md b/src/foundation/morphisms-cospan-diagrams.lagda.md index d1e4aa62c21..4e6184a65e2 100644 --- a/src/foundation/morphisms-cospan-diagrams.lagda.md +++ b/src/foundation/morphisms-cospan-diagrams.lagda.md @@ -59,11 +59,11 @@ module _ where left-map-hom-cospan-diagram : - left-type-cospan-diagram 𝒮 → left-type-cospan-diagram 𝒯 + domain-cospan-diagram 𝒮 → domain-cospan-diagram 𝒯 left-map-hom-cospan-diagram = pr1 h right-map-hom-cospan-diagram : - right-type-cospan-diagram 𝒮 → right-type-cospan-diagram 𝒯 + codomain-cospan-diagram 𝒮 → codomain-cospan-diagram 𝒯 right-map-hom-cospan-diagram = pr1 (pr2 h) cospanning-map-hom-cospan-diagram : @@ -131,9 +131,9 @@ module _ hom-cospan-diagram-rotate : (h : hom-cospan-diagram 𝒯 𝒮) (h' : hom-cospan-diagram ℛ 𝒮) → hom-cospan-diagram - ( left-type-cospan-diagram 𝒯 , - left-type-cospan-diagram ℛ , - left-type-cospan-diagram 𝒮 , + ( domain-cospan-diagram 𝒯 , + domain-cospan-diagram ℛ , + domain-cospan-diagram 𝒮 , left-map-hom-cospan-diagram 𝒯 𝒮 h , left-map-hom-cospan-diagram ℛ 𝒮 h') ( codomain-hom-cospan-diagram-rotate h h') @@ -149,9 +149,9 @@ module _ hom-cospan-diagram-rotate' : (h : hom-cospan-diagram 𝒯 𝒮) (h' : hom-cospan-diagram ℛ 𝒮) → hom-cospan-diagram - ( right-type-cospan-diagram 𝒯 , - right-type-cospan-diagram ℛ , - right-type-cospan-diagram 𝒮 , + ( codomain-cospan-diagram 𝒯 , + codomain-cospan-diagram ℛ , + codomain-cospan-diagram 𝒮 , right-map-hom-cospan-diagram 𝒯 𝒮 h , right-map-hom-cospan-diagram ℛ 𝒮 h') ( codomain-hom-cospan-diagram-rotate h h') diff --git a/src/foundation/morphisms-cospans.lagda.md b/src/foundation/morphisms-cospans.lagda.md index b3cdf33eb6a..64fd44b3715 100644 --- a/src/foundation/morphisms-cospans.lagda.md +++ b/src/foundation/morphisms-cospans.lagda.md @@ -47,13 +47,13 @@ module _ where coherence-hom-cospan : - (codomain-cospan c → codomain-cospan d) → UU (l1 ⊔ l2 ⊔ l4) + (cospanning-type-cospan c → cospanning-type-cospan d) → UU (l1 ⊔ l2 ⊔ l4) coherence-hom-cospan h = ( coherence-triangle-maps (left-map-cospan d) h (left-map-cospan c)) × ( coherence-triangle-maps (right-map-cospan d) h (right-map-cospan c)) hom-cospan : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) hom-cospan = - Σ ( codomain-cospan c → codomain-cospan d) + Σ ( cospanning-type-cospan c → cospanning-type-cospan d) ( coherence-hom-cospan) ``` diff --git a/src/foundation/pullback-cones.lagda.md b/src/foundation/pullback-cones.lagda.md index f35b29848dd..22cbef99c49 100644 --- a/src/foundation/pullback-cones.lagda.md +++ b/src/foundation/pullback-cones.lagda.md @@ -88,7 +88,7 @@ module _ cone-pullback-cone = pr2 (pr1 c) vertical-map-pullback-cone : - domain-pullback-cone → left-type-cospan-diagram 𝒮 + domain-pullback-cone → domain-cospan-diagram 𝒮 vertical-map-pullback-cone = vertical-map-cone ( left-map-cospan-diagram 𝒮) @@ -96,7 +96,7 @@ module _ ( cone-pullback-cone) horizontal-map-pullback-cone : - domain-pullback-cone → right-type-cospan-diagram 𝒮 + domain-pullback-cone → codomain-cospan-diagram 𝒮 horizontal-map-pullback-cone = horizontal-map-cone ( left-map-cospan-diagram 𝒮) diff --git a/src/orthogonal-factorization-systems/localizations-at-global-subuniverses.lagda.md b/src/orthogonal-factorization-systems/localizations-at-global-subuniverses.lagda.md index 94a477b5ada..488c8bf339d 100644 --- a/src/orthogonal-factorization-systems/localizations-at-global-subuniverses.lagda.md +++ b/src/orthogonal-factorization-systems/localizations-at-global-subuniverses.lagda.md @@ -490,24 +490,24 @@ module _ is-equiv-map-compute-cone-pullback-localization-global-subuniverse : is-in-global-subuniverse 𝒫 (cospanning-type-cospan-diagram 𝒮) → - is-in-global-subuniverse 𝒫 (left-type-cospan-diagram 𝒮) → - is-in-global-subuniverse 𝒫 (right-type-cospan-diagram 𝒮) → + is-in-global-subuniverse 𝒫 (domain-cospan-diagram 𝒮) → + is-in-global-subuniverse 𝒫 (codomain-cospan-diagram 𝒮) → is-equiv map-compute-cone-pullback-localization-global-subuniverse is-equiv-map-compute-cone-pullback-localization-global-subuniverse x a b = is-equiv-map-Σ _ ( up-localization-global-subuniverse LC - ( left-type-cospan-diagram 𝒮 , a)) + ( domain-cospan-diagram 𝒮 , a)) ( λ _ → is-equiv-map-Σ _ ( up-localization-global-subuniverse LC - ( right-type-cospan-diagram 𝒮 , b)) + ( codomain-cospan-diagram 𝒮 , b)) ( λ _ → is-equiv-right-whisker-unit-localization-global-subuniverse 𝒫 LC x)) is-in-global-subuniverse-pullback-localization-global-subuniverse : is-in-global-subuniverse 𝒫 (cospanning-type-cospan-diagram 𝒮) → - is-in-global-subuniverse 𝒫 (left-type-cospan-diagram 𝒮) → - is-in-global-subuniverse 𝒫 (right-type-cospan-diagram 𝒮) → + is-in-global-subuniverse 𝒫 (domain-cospan-diagram 𝒮) → + is-in-global-subuniverse 𝒫 (codomain-cospan-diagram 𝒮) → is-in-global-subuniverse 𝒫 (domain-pullback-cone 𝒮 c) is-in-global-subuniverse-pullback-localization-global-subuniverse x a b = is-in-global-subuniverse-is-local-type-universal-property-localization-global-subuniverse diff --git a/src/orthogonal-factorization-systems/reflective-global-subuniverses.lagda.md b/src/orthogonal-factorization-systems/reflective-global-subuniverses.lagda.md index 787a9630516..343258360c5 100644 --- a/src/orthogonal-factorization-systems/reflective-global-subuniverses.lagda.md +++ b/src/orthogonal-factorization-systems/reflective-global-subuniverses.lagda.md @@ -376,8 +376,8 @@ module _ is-in-reflective-global-subuniverse-pullback : is-in-reflective-global-subuniverse 𝒫 (cospanning-type-cospan-diagram 𝒮) → - is-in-reflective-global-subuniverse 𝒫 (left-type-cospan-diagram 𝒮) → - is-in-reflective-global-subuniverse 𝒫 (right-type-cospan-diagram 𝒮) → + is-in-reflective-global-subuniverse 𝒫 (domain-cospan-diagram 𝒮) → + is-in-reflective-global-subuniverse 𝒫 (codomain-cospan-diagram 𝒮) → is-in-reflective-global-subuniverse 𝒫 (domain-pullback-cone 𝒮 c) is-in-reflective-global-subuniverse-pullback = is-in-global-subuniverse-pullback-localization-global-subuniverse From 053b79a946c7bb20dc6d38b3eec574626fea18b4 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 28 Nov 2025 15:07:07 +0000 Subject: [PATCH 02/12] fixes --- src/foundation/operations-spans.lagda.md | 3 +-- src/synthetic-homotopy-theory/coforks.lagda.md | 9 ++++++--- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/src/foundation/operations-spans.lagda.md b/src/foundation/operations-spans.lagda.md index 6562513941e..31d310e4287 100644 --- a/src/foundation/operations-spans.lagda.md +++ b/src/foundation/operations-spans.lagda.md @@ -93,8 +93,7 @@ Consider a span `s` given by A <----- S -----> B ``` -and a [morphism of arrows](foundation.morphisms-arrows.md) `h : hom-arrow g' g` -as indicated in the diagram +and a equivalence of arrows `h : equiv-arrow g' g` as indicated in the diagram ```text g' diff --git a/src/synthetic-homotopy-theory/coforks.lagda.md b/src/synthetic-homotopy-theory/coforks.lagda.md index 34222f1a4f8..7843788621a 100644 --- a/src/synthetic-homotopy-theory/coforks.lagda.md +++ b/src/synthetic-homotopy-theory/coforks.lagda.md @@ -47,7 +47,8 @@ map `e : B → X` together with a [homotopy](foundation.homotopies.md) ```text g -----> e - A -----> B -----> X + A B -----> X + -----> f ``` @@ -120,7 +121,8 @@ a new cofork `h ∘ e`. ```text g -----> e h - A -----> B -----> X -----> Y + A B -----> X -----> Y + -----> f ``` @@ -198,7 +200,8 @@ module _ ```text g -----> e h k - A -----> B -----> X -----> Y -----> Z + A B -----> X -----> Y -----> Z + -----> f ``` From c8d025b06135c71daab040de58ff16f7216bed06 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 28 Nov 2025 16:07:05 +0000 Subject: [PATCH 03/12] operations on cospans --- src/foundation-core.lagda.md | 2 + .../operations-cospan-diagrams.lagda.md | 266 ++++++++++++++++++ .../operations-cospans.lagda.md | 219 ++++++++++++++ src/foundation.lagda.md | 4 + .../operations-cospan-diagrams.lagda.md | 168 +++++++++++ src/foundation/operations-cospans.lagda.md | 142 ++++++++++ src/foundation/opposite-cospans.lagda.md | 52 ++++ .../transposition-cospan-diagrams.lagda.md | 58 ++++ 8 files changed, 911 insertions(+) create mode 100644 src/foundation-core/operations-cospan-diagrams.lagda.md create mode 100644 src/foundation-core/operations-cospans.lagda.md create mode 100644 src/foundation/operations-cospan-diagrams.lagda.md create mode 100644 src/foundation/operations-cospans.lagda.md create mode 100644 src/foundation/opposite-cospans.lagda.md create mode 100644 src/foundation/transposition-cospan-diagrams.lagda.md diff --git a/src/foundation-core.lagda.md b/src/foundation-core.lagda.md index 8291e2bc800..5d5fe0818ea 100644 --- a/src/foundation-core.lagda.md +++ b/src/foundation-core.lagda.md @@ -39,6 +39,8 @@ open import foundation-core.injective-maps public open import foundation-core.invertible-maps public open import foundation-core.iterating-functions public open import foundation-core.negation public +open import foundation-core.operations-cospan-diagrams public +open import foundation-core.operations-cospans public open import foundation-core.operations-span-diagrams public open import foundation-core.operations-spans public open import foundation-core.path-split-maps public diff --git a/src/foundation-core/operations-cospan-diagrams.lagda.md b/src/foundation-core/operations-cospan-diagrams.lagda.md new file mode 100644 index 00000000000..9bae2fb230d --- /dev/null +++ b/src/foundation-core/operations-cospan-diagrams.lagda.md @@ -0,0 +1,266 @@ +# Operations on cospan diagrams + +```agda +module foundation-core.operations-cospan-diagrams where +``` + +
Imports + +```agda +open import foundation.cospan-diagrams +open import foundation.cospans +open import foundation.dependent-pair-types +open import foundation.morphisms-arrows +open import foundation.operations-cospans +open import foundation.universe-levels + +open import foundation-core.function-types +``` + +
+ +## Idea + +This file contains some operations on +[cospan diagrams](foundation.cospan-diagrams.md) that produce new cospan +diagrams from given cospan diagrams and possibly other data. + +## Definitions + +### Concatenating cospan diagrams and maps on both sides + +Consider a [cospan diagram](foundation.cospan-diagrams.md) `𝒮` given by + +```text + f g + A ------> S <------ B +``` + +and maps `i : A' → A` and `j : B' → B`. The +{{#concept "concatenation-cospan-diagram" Disambiguation="cospan diagram" Agda=concat-cospan-diagram}} +of `𝒮`, `i`, and `j` is the cospan diagram + +```text + f ∘ i g ∘ j + A' <------- S -------> B'. +``` + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} + where + + concat-cospan-diagram : + (𝒮 : cospan-diagram l1 l2 l3) + {A' : UU l4} (f : A' → domain-cospan-diagram 𝒮) + {B' : UU l5} (g : B' → codomain-cospan-diagram 𝒮) → + cospan-diagram l4 l5 l3 + pr1 (concat-cospan-diagram 𝒮 {A'} f {B'} g) = + A' + pr1 (pr2 (concat-cospan-diagram 𝒮 {A'} f {B'} g)) = + B' + pr2 (pr2 (concat-cospan-diagram 𝒮 {A'} f {B'} g)) = + concat-cospan (cospan-cospan-diagram 𝒮) f g +``` + +### Concatenating cospan diagrams and maps on the left + +Consider a [cospan diagram](foundation.cospan-diagrams.md) `𝒮` given by + +```text + f g + A ------> S <------ B +``` + +and a map `i : A' → A`. The +{{#concept "left concatenation" Disambiguation="cospan diagram" Agda=left-concat-cospan-diagram}} +of `𝒮` and `i` is the cospan diagram + +```text + f ∘ i g + A' <------- S -----> B. +``` + +```agda +module _ + {l1 l2 l3 l4 : Level} + where + + left-concat-cospan-diagram : + (𝒮 : cospan-diagram l1 l2 l3) {A' : UU l4} → + (A' → domain-cospan-diagram 𝒮) → cospan-diagram l4 l2 l3 + left-concat-cospan-diagram 𝒮 f = concat-cospan-diagram 𝒮 f id +``` + +### Concatenating cospan diagrams and maps on the right + +Consider a [cospan diagram](foundation.cospan-diagrams.md) `𝒮` given by + +```text + f g + A ------> S <------ B +``` + +and a map `j : B' → B`. The +{{#concept "right concatenation" Disambiguation="cospan diagram" Agda=right-concat-cospan-diagram}} +of `𝒮` by `j` is the cospan diagram + +```text + f g ∘ j + A' <----- S -------> B'. +``` + +```agda +module _ + {l1 l2 l3 l4 : Level} + where + + right-concat-cospan-diagram : + (𝒮 : cospan-diagram l1 l2 l3) {B' : UU l4} → + (B' → codomain-cospan-diagram 𝒮) → cospan-diagram l1 l4 l3 + right-concat-cospan-diagram 𝒮 g = concat-cospan-diagram 𝒮 id g +``` + +### Concatenation of cospan diagrams and morphisms of arrows on the left + +Consider a cospan diagram `𝒮` given by + +```text + f g + A ------> S <------ B +``` + +and a [morphism of arrows](foundation.morphisms-arrows.md) `h : hom-arrow f' f` +as indicated in the diagram + +```text + f g + A ------> S <------ B. + | | + h₀ | | h₁ + ∨ ∨ + A' <----- S' + f' +``` + +Then we obtain a cospan diagram `A' --> S' <-- B`. + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} (𝒮 : cospan-diagram l1 l2 l3) + {S' : UU l4} {A' : UU l5} (f' : A' → S') + (h : hom-arrow (left-map-cospan-diagram 𝒮) f') + where + + domain-left-concat-hom-arrow-cospan-diagram : UU l5 + domain-left-concat-hom-arrow-cospan-diagram = A' + + codomain-left-concat-hom-arrow-cospan-diagram : UU l2 + codomain-left-concat-hom-arrow-cospan-diagram = codomain-cospan-diagram 𝒮 + + cospan-left-concat-hom-arrow-cospan-diagram : + cospan l4 + ( domain-left-concat-hom-arrow-cospan-diagram) + ( codomain-left-concat-hom-arrow-cospan-diagram) + cospan-left-concat-hom-arrow-cospan-diagram = + left-concat-hom-arrow-cospan + ( cospan-cospan-diagram 𝒮) + ( f') + ( h) + + left-concat-hom-arrow-cospan-diagram : cospan-diagram l5 l2 l4 + pr1 left-concat-hom-arrow-cospan-diagram = + domain-left-concat-hom-arrow-cospan-diagram + pr1 (pr2 left-concat-hom-arrow-cospan-diagram) = + codomain-left-concat-hom-arrow-cospan-diagram + pr2 (pr2 left-concat-hom-arrow-cospan-diagram) = + cospan-left-concat-hom-arrow-cospan-diagram + + cospanning-type-left-concat-hom-arrow-cospan-diagram : UU l4 + cospanning-type-left-concat-hom-arrow-cospan-diagram = + cospanning-type-cospan-diagram left-concat-hom-arrow-cospan-diagram + + left-map-left-concat-hom-arrow-cospan-diagram : + domain-left-concat-hom-arrow-cospan-diagram → + cospanning-type-left-concat-hom-arrow-cospan-diagram + left-map-left-concat-hom-arrow-cospan-diagram = + left-map-cospan-diagram left-concat-hom-arrow-cospan-diagram + + right-map-left-concat-hom-arrow-cospan-diagram : + codomain-left-concat-hom-arrow-cospan-diagram → + cospanning-type-left-concat-hom-arrow-cospan-diagram + right-map-left-concat-hom-arrow-cospan-diagram = + right-map-cospan-diagram left-concat-hom-arrow-cospan-diagram +``` + +### Concatenation of cospan diagrams and morphisms of arrows on the right + +Consider a cospan diagram `𝒮` given by + +```text + f g + A ------> S <------ B +``` + +and a [morphism of arrows](foundation.morphisms-arrows.md) `h : hom-arrow g' g` +as indicated in the diagram + +```text + f g + A ------> S <------ B. + | | + h₀ | | h₁ + ∨ ∨ + S' <----- B' + g' +``` + +Then we obtain a cospan diagram `A --> S' <-- B'`. + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} (𝒮 : cospan-diagram l1 l2 l3) + {S' : UU l4} {B' : UU l5} (g' : B' → S') + (h : hom-arrow (right-map-cospan-diagram 𝒮) g') + where + + domain-right-concat-hom-arrow-cospan-diagram : UU l1 + domain-right-concat-hom-arrow-cospan-diagram = domain-cospan-diagram 𝒮 + + codomain-right-concat-hom-arrow-cospan-diagram : UU l5 + codomain-right-concat-hom-arrow-cospan-diagram = B' + + cospan-right-concat-hom-arrow-cospan-diagram : + cospan l4 + ( domain-right-concat-hom-arrow-cospan-diagram) + ( codomain-right-concat-hom-arrow-cospan-diagram) + cospan-right-concat-hom-arrow-cospan-diagram = + right-concat-hom-arrow-cospan + ( cospan-cospan-diagram 𝒮) + ( g') + ( h) + + right-concat-hom-arrow-cospan-diagram : cospan-diagram l1 l5 l4 + pr1 right-concat-hom-arrow-cospan-diagram = + domain-right-concat-hom-arrow-cospan-diagram + pr1 (pr2 right-concat-hom-arrow-cospan-diagram) = + codomain-right-concat-hom-arrow-cospan-diagram + pr2 (pr2 right-concat-hom-arrow-cospan-diagram) = + cospan-right-concat-hom-arrow-cospan-diagram + + cospanning-type-right-concat-hom-arrow-cospan-diagram : UU l4 + cospanning-type-right-concat-hom-arrow-cospan-diagram = + cospanning-type-cospan-diagram right-concat-hom-arrow-cospan-diagram + + left-map-right-concat-hom-arrow-cospan-diagram : + domain-right-concat-hom-arrow-cospan-diagram → + cospanning-type-right-concat-hom-arrow-cospan-diagram + left-map-right-concat-hom-arrow-cospan-diagram = + left-map-cospan-diagram right-concat-hom-arrow-cospan-diagram + + right-map-right-concat-hom-arrow-cospan-diagram : + codomain-right-concat-hom-arrow-cospan-diagram → + cospanning-type-right-concat-hom-arrow-cospan-diagram + right-map-right-concat-hom-arrow-cospan-diagram = + right-map-cospan-diagram right-concat-hom-arrow-cospan-diagram +``` diff --git a/src/foundation-core/operations-cospans.lagda.md b/src/foundation-core/operations-cospans.lagda.md new file mode 100644 index 00000000000..c4f37dc5583 --- /dev/null +++ b/src/foundation-core/operations-cospans.lagda.md @@ -0,0 +1,219 @@ +# Operations on cospans + +```agda +module foundation-core.operations-cospans where +``` + +
Imports + +```agda +open import foundation.cospans +open import foundation.dependent-pair-types +open import foundation.morphisms-arrows +open import foundation.universe-levels + +open import foundation-core.function-types +``` + +
+ +## Idea + +This file contains some operations on [cospans](foundation.cospans.md) that +produce new cospans from given cospans and possibly other data. + +## Definitions + +### Concatenating cospans and maps on both sides + +Consider a [cospan](foundation.cospans.md) `s` given by + +```text + f g + A ------> S <------ B +``` + +and maps `i : A' → A` and `j : B' → B`. The +{{#concept "concatenation cospan" Disambiguation="cospan" Agda=concat-cospan}} +of `i`, `s`, and `j` is the cospan + +```text + f ∘ i g ∘ j + A' ------> S <------ B. +``` + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} + {A : UU l1} {A' : UU l2} + {B : UU l3} {B' : UU l4} + where + + concat-cospan : cospan l5 A B → (A' → A) → (B' → B) → cospan l5 A' B' + pr1 (concat-cospan s i j) = cospanning-type-cospan s + pr1 (pr2 (concat-cospan s i j)) = left-map-cospan s ∘ i + pr2 (pr2 (concat-cospan s i j)) = right-map-cospan s ∘ j +``` + +### Concatenating cospans and maps on the left + +Consider a [cospan](foundation.cospans.md) `s` given by + +```text + f g + A ------> S <------ B +``` + +and a map `i : A' → A`. The +{{#concept "left concatenation" Disambiguation="cospan" Agda=left-concat-cospan}} +of `s` by `i` is the cospan + +```text + f ∘ i g + A' ------> S <------ B. +``` + +```agda +module _ + {l1 l2 l3 l4 : Level} + {A : UU l1} {A' : UU l2} {B : UU l3} + where + + left-concat-cospan : cospan l4 A B → (A' → A) → cospan l4 A' B + left-concat-cospan s f = concat-cospan s f id +``` + +### Concatenating cospans and maps on the right + +Consider a [cospan](foundation.cospans.md) `s` given by + +```text + f g + A ------> S <------ B +``` + +and a map `j : B' → B`. The +{{#concept "right concatenation" Disambiguation="cospan" Agda=right-concat-cospan}} +of `s` by `j` is the cospan + +```text + f g ∘ j + A' <------ S ------> B. +``` + +```agda +module _ + {l1 l2 l3 l4 : Level} + {A : UU l1} + {B : UU l3} {B' : UU l4} + where + + right-concat-cospan : cospan l4 A B → (B' → B) → cospan l4 A B' + right-concat-cospan s g = concat-cospan s id g +``` + +### Concatenating cospans and morphisms of arrows on the left + +Consider a cospan `s` given by + +```text + f g + A -----> S <----- B +``` + +and a [morphism of arrows](foundation.morphisms-arrows.md) `h : hom-arrow f f'` +as indicated in the diagram + +```text + f g + A ------> S <------ B. + | | + h₀ | | h₁ + ∨ ∨ + A' -----> S' + f' +``` + +Then we obtain a cospan `A' --> S' <-- B`. + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} + {A : UU l1} {B : UU l2} (s : cospan l3 A B) + {S' : UU l4} {A' : UU l5} (f' : A' → S') + (h : hom-arrow (left-map-cospan s) f') + where + + cospanning-type-left-concat-hom-arrow-cospan : UU l4 + cospanning-type-left-concat-hom-arrow-cospan = S' + + left-map-left-concat-hom-arrow-cospan : + A' → cospanning-type-left-concat-hom-arrow-cospan + left-map-left-concat-hom-arrow-cospan = f' + + right-map-left-concat-hom-arrow-cospan : + B → cospanning-type-left-concat-hom-arrow-cospan + right-map-left-concat-hom-arrow-cospan = + map-codomain-hom-arrow (left-map-cospan s) f' h ∘ right-map-cospan s + + left-concat-hom-arrow-cospan : cospan l4 A' B + pr1 left-concat-hom-arrow-cospan = + cospanning-type-left-concat-hom-arrow-cospan + pr1 (pr2 left-concat-hom-arrow-cospan) = + left-map-left-concat-hom-arrow-cospan + pr2 (pr2 left-concat-hom-arrow-cospan) = + right-map-left-concat-hom-arrow-cospan +``` + +### Concatenating cospans and morphisms of arrows on the right + +Consider a cospan `s` given by + +```text + f g + A ------> S <------ B +``` + +and a [morphism of arrows](foundation.morphisms-arrows.md) `h : hom-arrow g' g` +as indicated in the diagram + +```text + f g + A ------> S <------ B + | | + h₀ | | h₁ + ∨ ∨ + S' -----> B'. + g' +``` + +Then we obtain a cospan `A --> S' <-- B'`. + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} + (s : cospan l3 A B) + {S' : UU l4} {B' : UU l5} (g' : B' → S') + (h : hom-arrow (right-map-cospan s) g') + where + + cospanning-type-right-concat-hom-arrow-cospan : UU l4 + cospanning-type-right-concat-hom-arrow-cospan = S' + + left-map-right-concat-hom-arrow-cospan : + A → cospanning-type-right-concat-hom-arrow-cospan + left-map-right-concat-hom-arrow-cospan = + map-codomain-hom-arrow (right-map-cospan s) g' h ∘ left-map-cospan s + + right-map-right-concat-hom-arrow-cospan : + B' → cospanning-type-right-concat-hom-arrow-cospan + right-map-right-concat-hom-arrow-cospan = g' + + right-concat-hom-arrow-cospan : cospan l4 A B' + pr1 right-concat-hom-arrow-cospan = + cospanning-type-right-concat-hom-arrow-cospan + pr1 (pr2 right-concat-hom-arrow-cospan) = + left-map-right-concat-hom-arrow-cospan + pr2 (pr2 right-concat-hom-arrow-cospan) = + right-map-right-concat-hom-arrow-cospan +``` diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index 931de9244e3..40e20ba6dce 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -339,9 +339,12 @@ open import foundation.negation public open import foundation.noncontractible-types public open import foundation.noninjective-maps public open import foundation.null-homotopic-maps public +open import foundation.operations-cospan-diagrams public +open import foundation.operations-cospans public open import foundation.operations-span-diagrams public open import foundation.operations-spans public open import foundation.operations-spans-families-of-types public +open import foundation.opposite-cospans public open import foundation.opposite-spans public open import foundation.pairs-of-distinct-elements public open import foundation.partial-elements public @@ -458,6 +461,7 @@ open import foundation.transport-along-higher-identifications public open import foundation.transport-along-homotopies public open import foundation.transport-along-identifications public open import foundation.transport-split-type-families public +open import foundation.transposition-cospan-diagrams public open import foundation.transposition-identifications-along-equivalences public open import foundation.transposition-identifications-along-retractions public open import foundation.transposition-identifications-along-sections public diff --git a/src/foundation/operations-cospan-diagrams.lagda.md b/src/foundation/operations-cospan-diagrams.lagda.md new file mode 100644 index 00000000000..73aae85aa48 --- /dev/null +++ b/src/foundation/operations-cospan-diagrams.lagda.md @@ -0,0 +1,168 @@ +# Operations on cospan diagrams + +```agda +module foundation.operations-cospan-diagrams where + +open import foundation-core.operations-cospan-diagrams public +``` + +
Imports + +```agda +open import foundation.cospan-diagrams +open import foundation.cospans +open import foundation.dependent-pair-types +open import foundation.equivalences-arrows +open import foundation.operations-cospans +open import foundation.universe-levels +``` + +
+ +## Idea + +This file contains some further operations on +[cospan diagrams](foundation.cospan-diagrams.md) that produce new cospan +diagrams from given cospan diagrams and possibly other data. Previous operations +on cospan diagrams were defined in +[`foundation-core.operations-cospan-diagrams`](foundation-core.operations-cospan-diagrams.md). + +## Definitions + +### Concatenating cospan diagrams and equivalences of arrows on the left + +Consider a cospan diagram `𝒮` given by + +```text + f g + A ------> S <------ B +``` + +and an [equivalence of arrows](foundation.equivalences-arrows.md) +`h : equiv-arrow f' f` as indicated in the diagram + +```text + f g + A ------> S <------ B. + | | + h₀ | ≃ ≃ | h₁ + ∨ ∨ + A' -----> S' + f' +``` + +Then we obtain a cospan diagram `A' --> S' <-- B`. + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} (𝒮 : cospan-diagram l1 l2 l3) + {S' : UU l4} {A' : UU l5} (f' : A' → S') + (h : equiv-arrow (left-map-cospan-diagram 𝒮) f') + where + + domain-left-concat-equiv-arrow-cospan-diagram : UU l5 + domain-left-concat-equiv-arrow-cospan-diagram = A' + + codomain-left-concat-equiv-arrow-cospan-diagram : UU l2 + codomain-left-concat-equiv-arrow-cospan-diagram = codomain-cospan-diagram 𝒮 + + cospan-left-concat-equiv-arrow-cospan-diagram : + cospan l4 + ( domain-left-concat-equiv-arrow-cospan-diagram) + ( codomain-left-concat-equiv-arrow-cospan-diagram) + cospan-left-concat-equiv-arrow-cospan-diagram = + left-concat-equiv-arrow-cospan (cospan-cospan-diagram 𝒮) f' h + + left-concat-equiv-arrow-cospan-diagram : cospan-diagram l5 l2 l4 + pr1 left-concat-equiv-arrow-cospan-diagram = + domain-left-concat-equiv-arrow-cospan-diagram + pr1 (pr2 left-concat-equiv-arrow-cospan-diagram) = + codomain-left-concat-equiv-arrow-cospan-diagram + pr2 (pr2 left-concat-equiv-arrow-cospan-diagram) = + cospan-left-concat-equiv-arrow-cospan-diagram + + cospanning-type-left-concat-equiv-arrow-cospan-diagram : UU l4 + cospanning-type-left-concat-equiv-arrow-cospan-diagram = + cospanning-type-cospan-diagram left-concat-equiv-arrow-cospan-diagram + + left-map-left-concat-equiv-arrow-cospan-diagram : + domain-left-concat-equiv-arrow-cospan-diagram → + cospanning-type-left-concat-equiv-arrow-cospan-diagram + left-map-left-concat-equiv-arrow-cospan-diagram = + left-map-cospan-diagram left-concat-equiv-arrow-cospan-diagram + + right-map-left-concat-equiv-arrow-cospan-diagram : + codomain-left-concat-equiv-arrow-cospan-diagram → + cospanning-type-left-concat-equiv-arrow-cospan-diagram + right-map-left-concat-equiv-arrow-cospan-diagram = + right-map-cospan-diagram left-concat-equiv-arrow-cospan-diagram +``` + +### Concatenating cospan diagrams and equivalences of arrows on the right + +Consider a cospan diagram `𝒮` given by + +```text + f g + A ------> S <------ B +``` + +and a [equivalence of arrows](foundation.equivalences-arrows.md) +`h : equiv-arrow g' g` as indicated in the diagram + +```text + f g + A ------> S <------ B. + | | + h₀ | ≃ ≃ | h₁ + ∨ ∨ + S' <----- B' + g' +``` + +Then we obtain a cospan diagram `A --> S' <-- B'`. + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} (𝒮 : cospan-diagram l1 l2 l3) + {S' : UU l4} {B' : UU l5} (g' : B' → S') + (h : equiv-arrow (right-map-cospan-diagram 𝒮) g') + where + + domain-right-concat-equiv-arrow-cospan-diagram : UU l1 + domain-right-concat-equiv-arrow-cospan-diagram = domain-cospan-diagram 𝒮 + + codomain-right-concat-equiv-arrow-cospan-diagram : UU l5 + codomain-right-concat-equiv-arrow-cospan-diagram = B' + + cospan-right-concat-equiv-arrow-cospan-diagram : + cospan l4 + ( domain-right-concat-equiv-arrow-cospan-diagram) + ( codomain-right-concat-equiv-arrow-cospan-diagram) + cospan-right-concat-equiv-arrow-cospan-diagram = + right-concat-equiv-arrow-cospan (cospan-cospan-diagram 𝒮) g' h + + right-concat-equiv-arrow-cospan-diagram : cospan-diagram l1 l5 l4 + pr1 right-concat-equiv-arrow-cospan-diagram = + domain-right-concat-equiv-arrow-cospan-diagram + pr1 (pr2 right-concat-equiv-arrow-cospan-diagram) = + codomain-right-concat-equiv-arrow-cospan-diagram + pr2 (pr2 right-concat-equiv-arrow-cospan-diagram) = + cospan-right-concat-equiv-arrow-cospan-diagram + + cospanning-type-right-concat-equiv-arrow-cospan-diagram : UU l4 + cospanning-type-right-concat-equiv-arrow-cospan-diagram = + cospanning-type-cospan-diagram right-concat-equiv-arrow-cospan-diagram + + left-map-right-concat-equiv-arrow-cospan-diagram : + domain-right-concat-equiv-arrow-cospan-diagram → + cospanning-type-right-concat-equiv-arrow-cospan-diagram + left-map-right-concat-equiv-arrow-cospan-diagram = + left-map-cospan-diagram right-concat-equiv-arrow-cospan-diagram + + right-map-right-concat-equiv-arrow-cospan-diagram : + codomain-right-concat-equiv-arrow-cospan-diagram → + cospanning-type-right-concat-equiv-arrow-cospan-diagram + right-map-right-concat-equiv-arrow-cospan-diagram = + right-map-cospan-diagram right-concat-equiv-arrow-cospan-diagram +``` diff --git a/src/foundation/operations-cospans.lagda.md b/src/foundation/operations-cospans.lagda.md new file mode 100644 index 00000000000..334bb7f3162 --- /dev/null +++ b/src/foundation/operations-cospans.lagda.md @@ -0,0 +1,142 @@ +# Operations on cospans + +```agda +module foundation.operations-cospans where + +open import foundation-core.operations-cospans public +``` + +
Imports + +```agda +open import foundation.cospans +open import foundation.dependent-pair-types +open import foundation.equivalences-arrows +open import foundation.morphisms-arrows +open import foundation.universe-levels + +open import foundation-core.function-types +``` + +
+ +## Idea + +This file contains some further operations on [cospans](foundation.cospans.md) +that produce new cospans from given cospans and possibly other data. Previous +operations on cospans were defined in +[`foundation-core.operations-cospans`](foundation-core.operations-cospans.md). + +## Definitions + +### Concatenating cospans and equivalences of arrows on the left + +Consider a cospan `s` given by + +```text + f g + A ------> S <------ B +``` + +and an [equivalence of arrows](foundation.equivalences-arrows.md) +`h : equiv-arrow f' f` as indicated in the diagram + +```text + f g + A ------> S <------ B. + | | + h₀ | ≃ ≃ | h₁ + ∨ ∨ + A' -----> S' + f' +``` + +Then we obtain a cospan `A' --> S' <-- B`. + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} + (s : cospan l3 A B) + {S' : UU l4} {A' : UU l5} (f' : A' → S') + (h : equiv-arrow (left-map-cospan s) f') + where + + cospanning-type-left-concat-equiv-arrow-cospan : UU l4 + cospanning-type-left-concat-equiv-arrow-cospan = S' + + left-map-left-concat-equiv-arrow-cospan : + A' → cospanning-type-left-concat-equiv-arrow-cospan + left-map-left-concat-equiv-arrow-cospan = f' + + right-map-left-concat-equiv-arrow-cospan : + B → cospanning-type-left-concat-equiv-arrow-cospan + right-map-left-concat-equiv-arrow-cospan = + map-codomain-equiv-arrow (left-map-cospan s) f' h ∘ right-map-cospan s + + left-concat-equiv-arrow-cospan : + cospan l4 A' B + pr1 left-concat-equiv-arrow-cospan = + cospanning-type-left-concat-equiv-arrow-cospan + pr1 (pr2 left-concat-equiv-arrow-cospan) = + left-map-left-concat-equiv-arrow-cospan + pr2 (pr2 left-concat-equiv-arrow-cospan) = + right-map-left-concat-equiv-arrow-cospan +``` + +### Concatenating cospans and equivalences of arrows on the right + +Consider a cospan `s` given by + +```text + f g + A ------> S <------ B +``` + +and an equivalence of arrows `h : equiv-arrow g' g` as indicated in the diagram + +```text + f g + A ------> S <------ B + | | + h₀ | ≃ ≃ | h₁ + ∨ ∨ + S' <----- B'. + g' +``` + +Then we obtain a cospan `A --> S' <-- B'`. + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} + (s : cospan l3 A B) + {S' : UU l4} {B' : UU l5} (g' : B' → S') + (h : equiv-arrow (right-map-cospan s) g') + where + + cospanning-type-right-concat-equiv-arrow-cospan : UU l4 + cospanning-type-right-concat-equiv-arrow-cospan = S' + + left-map-right-concat-equiv-arrow-cospan : + A → cospanning-type-right-concat-equiv-arrow-cospan + left-map-right-concat-equiv-arrow-cospan = + map-codomain-equiv-arrow (right-map-cospan s) g' h ∘ left-map-cospan s + + right-map-right-concat-equiv-arrow-cospan : + B' → cospanning-type-right-concat-equiv-arrow-cospan + right-map-right-concat-equiv-arrow-cospan = g' + + right-concat-equiv-arrow-cospan : + cospan l4 A B' + pr1 right-concat-equiv-arrow-cospan = + cospanning-type-right-concat-equiv-arrow-cospan + pr1 (pr2 right-concat-equiv-arrow-cospan) = + left-map-right-concat-equiv-arrow-cospan + pr2 (pr2 right-concat-equiv-arrow-cospan) = + right-map-right-concat-equiv-arrow-cospan +``` + +## See also + +- [Composition of cospans](foundation.composition-cospans.md) +- [Opposite cospans](foundation.opposite-cospans.md) diff --git a/src/foundation/opposite-cospans.lagda.md b/src/foundation/opposite-cospans.lagda.md new file mode 100644 index 00000000000..07ac51d7c09 --- /dev/null +++ b/src/foundation/opposite-cospans.lagda.md @@ -0,0 +1,52 @@ +# Opposite cospans + +```agda +module foundation.opposite-cospans where +``` + +
Imports + +```agda +open import foundation.cospans +open import foundation.dependent-pair-types +open import foundation.universe-levels +``` + +
+ +## Idea + +Consider a [cospan](foundation.cospans.md) `(S , f , g)` from `A` to `B`. The +{{#concept "opposite cospan" Agda=opposite-cospan}} of `(S , f , g)` is the +cospan `(S , g , f)` from `B` to `A`. In other words, the opposite of a cospan + +```text + f g + A ------> S <------ B +``` + +is the cospan + +```text + g f + B ------> S <------ A. +``` + +## Definitions + +### The opposite of a cospan + +```agda +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} + where + + opposite-cospan : cospan l3 A B → cospan l3 B A + pr1 (opposite-cospan s) = cospanning-type-cospan s + pr1 (pr2 (opposite-cospan s)) = right-map-cospan s + pr2 (pr2 (opposite-cospan s)) = left-map-cospan s +``` + +## See also + +- [Transpositions of cospan diagrams](foundation.transposition-cospan-diagrams.md) diff --git a/src/foundation/transposition-cospan-diagrams.lagda.md b/src/foundation/transposition-cospan-diagrams.lagda.md new file mode 100644 index 00000000000..330d7540876 --- /dev/null +++ b/src/foundation/transposition-cospan-diagrams.lagda.md @@ -0,0 +1,58 @@ +# Transposition of cospan diagrams + +```agda +module foundation.transposition-cospan-diagrams where +``` + +
Imports + +```agda +open import foundation.cospan-diagrams +open import foundation.cospans +open import foundation.dependent-pair-types +open import foundation.opposite-cospans +open import foundation.universe-levels +``` + +
+ +## Idea + +The +{{#concept "transposition" Disambiguation="cospan diagram" Agda=transposition-cospan-diagram}} +of a [cospan diagram](foundation.cospan-diagrams.md) + +```text + f g + A ------> S <------ B +``` + +is the cospan diagram + +```text + g f + B ------> S <------ A. +``` + +In other words, the transposition of a cospan diagram `(A , B , s)` is the +cospan diagram `(B , A , opposite-cospan s)` where `opposite-cospan s` is the +[opposite](foundation.opposite-cospans.md) of the +[cospan](foundation.cospans.md) `s` from `A` to `B`. + +## Definitions + +### Transposition of cospan diagrams + +```agda +module _ + {l1 l2 l3 : Level} (𝒮 : cospan-diagram l1 l2 l3) + where + + transposition-cospan-diagram : cospan-diagram l2 l1 l3 + pr1 transposition-cospan-diagram = + codomain-cospan-diagram 𝒮 + pr1 (pr2 transposition-cospan-diagram) = + domain-cospan-diagram 𝒮 + pr2 (pr2 transposition-cospan-diagram) = + opposite-cospan (cospan-cospan-diagram 𝒮) +``` From 2c25a32e787ee9f2be0f7708141b95300f713dbe Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 28 Nov 2025 16:11:24 +0000 Subject: [PATCH 04/12] fix diagrams --- .../operations-cospan-diagrams.lagda.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/foundation-core/operations-cospan-diagrams.lagda.md b/src/foundation-core/operations-cospan-diagrams.lagda.md index 9bae2fb230d..f991626ac53 100644 --- a/src/foundation-core/operations-cospan-diagrams.lagda.md +++ b/src/foundation-core/operations-cospan-diagrams.lagda.md @@ -41,8 +41,8 @@ and maps `i : A' → A` and `j : B' → B`. The of `𝒮`, `i`, and `j` is the cospan diagram ```text - f ∘ i g ∘ j - A' <------- S -------> B'. + f ∘ i g ∘ j + A' ------> S <------ B'. ``` ```agda @@ -77,8 +77,8 @@ and a map `i : A' → A`. The of `𝒮` and `i` is the cospan diagram ```text - f ∘ i g - A' <------- S -----> B. + f ∘ i g + A' ------> S <------ B. ``` ```agda @@ -106,8 +106,8 @@ and a map `j : B' → B`. The of `𝒮` by `j` is the cospan diagram ```text - f g ∘ j - A' <----- S -------> B'. + f g ∘ j + A' ------> S <------ B'. ``` ```agda @@ -139,7 +139,7 @@ as indicated in the diagram | | h₀ | | h₁ ∨ ∨ - A' <----- S' + A' -----> S' f' ``` From 5b8837868cc300b0b33181462525e568ae9b1be5 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 28 Nov 2025 16:18:09 +0000 Subject: [PATCH 05/12] fixes --- .../operations-cospan-diagrams.lagda.md | 12 ++++++------ src/foundation-core/operations-cospans.lagda.md | 6 +++--- .../operations-span-diagrams.lagda.md | 12 ++++++------ 3 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/foundation-core/operations-cospan-diagrams.lagda.md b/src/foundation-core/operations-cospan-diagrams.lagda.md index f991626ac53..7778dc6a38a 100644 --- a/src/foundation-core/operations-cospan-diagrams.lagda.md +++ b/src/foundation-core/operations-cospan-diagrams.lagda.md @@ -52,15 +52,15 @@ module _ concat-cospan-diagram : (𝒮 : cospan-diagram l1 l2 l3) - {A' : UU l4} (f : A' → domain-cospan-diagram 𝒮) - {B' : UU l5} (g : B' → codomain-cospan-diagram 𝒮) → + {A' : UU l4} (i : A' → domain-cospan-diagram 𝒮) + {B' : UU l5} (j : B' → codomain-cospan-diagram 𝒮) → cospan-diagram l4 l5 l3 - pr1 (concat-cospan-diagram 𝒮 {A'} f {B'} g) = + pr1 (concat-cospan-diagram 𝒮 {A'} i {B'} j) = A' - pr1 (pr2 (concat-cospan-diagram 𝒮 {A'} f {B'} g)) = + pr1 (pr2 (concat-cospan-diagram 𝒮 {A'} i {B'} j)) = B' - pr2 (pr2 (concat-cospan-diagram 𝒮 {A'} f {B'} g)) = - concat-cospan (cospan-cospan-diagram 𝒮) f g + pr2 (pr2 (concat-cospan-diagram 𝒮 {A'} i {B'} j)) = + concat-cospan (cospan-cospan-diagram 𝒮) i j ``` ### Concatenating cospan diagrams and maps on the left diff --git a/src/foundation-core/operations-cospans.lagda.md b/src/foundation-core/operations-cospans.lagda.md index c4f37dc5583..4b5c1f7ae52 100644 --- a/src/foundation-core/operations-cospans.lagda.md +++ b/src/foundation-core/operations-cospans.lagda.md @@ -98,7 +98,7 @@ of `s` by `j` is the cospan ```text f g ∘ j - A' <------ S ------> B. + A' ------> S <------ B. ``` ```agda @@ -117,8 +117,8 @@ module _ Consider a cospan `s` given by ```text - f g - A -----> S <----- B + f g + A ------> S <------ B ``` and a [morphism of arrows](foundation.morphisms-arrows.md) `h : hom-arrow f f'` diff --git a/src/foundation-core/operations-span-diagrams.lagda.md b/src/foundation-core/operations-span-diagrams.lagda.md index 78b68e8722c..f54aa595a5e 100644 --- a/src/foundation-core/operations-span-diagrams.lagda.md +++ b/src/foundation-core/operations-span-diagrams.lagda.md @@ -52,15 +52,15 @@ module _ concat-span-diagram : (𝒮 : span-diagram l1 l2 l3) - {A' : UU l4} (f : domain-span-diagram 𝒮 → A') - {B' : UU l5} (g : codomain-span-diagram 𝒮 → B') → + {A' : UU l4} (i : domain-span-diagram 𝒮 → A') + {B' : UU l5} (j : codomain-span-diagram 𝒮 → B') → span-diagram l4 l5 l3 - pr1 (concat-span-diagram 𝒮 {A'} f {B'} g) = + pr1 (concat-span-diagram 𝒮 {A'} i {B'} j) = A' - pr1 (pr2 (concat-span-diagram 𝒮 {A'} f {B'} g)) = + pr1 (pr2 (concat-span-diagram 𝒮 {A'} i {B'} j)) = B' - pr2 (pr2 (concat-span-diagram 𝒮 {A'} f {B'} g)) = - concat-span (span-span-diagram 𝒮) f g + pr2 (pr2 (concat-span-diagram 𝒮 {A'} i {B'} j)) = + concat-span (span-span-diagram 𝒮) i j ``` ### Concatenating span diagrams and maps on the left From bbbfcc04603e35385fe165c5d37b07030c0c6cc4 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 28 Nov 2025 16:31:31 +0000 Subject: [PATCH 06/12] Composition of cospans --- src/synthetic-homotopy-theory.lagda.md | 1 + .../composition-cospans.lagda.md | 90 +++++++++++++++++++ 2 files changed, 91 insertions(+) create mode 100644 src/synthetic-homotopy-theory/composition-cospans.lagda.md diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md index 2839f2a8162..01685d014b9 100644 --- a/src/synthetic-homotopy-theory.lagda.md +++ b/src/synthetic-homotopy-theory.lagda.md @@ -27,6 +27,7 @@ open import synthetic-homotopy-theory.cofibers-of-maps public open import synthetic-homotopy-theory.cofibers-of-pointed-maps public open import synthetic-homotopy-theory.coforks public open import synthetic-homotopy-theory.coforks-cocones-under-sequential-diagrams public +open import synthetic-homotopy-theory.composition-cospans public open import synthetic-homotopy-theory.conjugation-loops public open import synthetic-homotopy-theory.connected-set-bundles-circle public open import synthetic-homotopy-theory.connective-prespectra public diff --git a/src/synthetic-homotopy-theory/composition-cospans.lagda.md b/src/synthetic-homotopy-theory/composition-cospans.lagda.md new file mode 100644 index 00000000000..48f76fd478f --- /dev/null +++ b/src/synthetic-homotopy-theory/composition-cospans.lagda.md @@ -0,0 +1,90 @@ +# Composition of cospans + +```agda +module synthetic-homotopy-theory.composition-cospans where +``` + +
Imports + +```agda +open import foundation.commuting-triangles-of-maps +open import foundation.cospans +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.equivalences-arrows +open import foundation.equivalences-cospans +open import foundation.homotopies +open import foundation.identity-types +open import foundation.morphisms-arrows +open import foundation.morphisms-cospans +open import foundation.pullbacks +open import foundation.standard-pullbacks +open import foundation.type-arithmetic-standard-pullbacks +open import foundation.universe-levels + +open import foundation-core.function-types + +open import synthetic-homotopy-theory.pushouts +``` + +
+ +## Idea + +Given two [cospans](foundation.cospans.md) `F` and `G` such that the source of +`G` is the target of `F` + +```text + F G + + A -----> S <----- B -----> T <----- C, +``` + +then we may +{{#concept "compose" Disambiguation="cospans of types" Agda=comp-cospan}} the +two cospans by forming the [pushout](synthetic-homotopy-theory.pushouts.md) of +the middle [cospan diagram](foundation.cospan-diagrams.md) + +```text + C + | + | + ∨ + B ------> T + | | + | | + ∨ ⌜ ∨ + A ------> S ------> ∙ +``` + +giving us a cospan `G ∘ F` from `A` to `C`. + +## Definitions + +### Composition of cospans + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} + {A : UU l1} {B : UU l2} {C : UU l3} + (G : cospan l4 B C) (F : cospan l5 A B) + where + + cospanning-type-comp-cospan : UU (l2 ⊔ l4 ⊔ l5) + cospanning-type-comp-cospan = + pushout (right-map-cospan F) (left-map-cospan G) + + left-map-comp-cospan : A → cospanning-type-comp-cospan + left-map-comp-cospan = + inl-pushout (right-map-cospan F) (left-map-cospan G) ∘ left-map-cospan F + + right-map-comp-cospan : C → cospanning-type-comp-cospan + right-map-comp-cospan = + inr-pushout (right-map-cospan F) (left-map-cospan G) ∘ right-map-cospan G + + comp-cospan : cospan (l2 ⊔ l4 ⊔ l5) A C + comp-cospan = + ( cospanning-type-comp-cospan , + left-map-comp-cospan , + right-map-comp-cospan) +``` From e173469c82796299ec388c1b2caede0626a6136b Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 28 Nov 2025 16:31:59 +0000 Subject: [PATCH 07/12] indentation --- .../composition-cospans.lagda.md | 29 ++++++------------- 1 file changed, 9 insertions(+), 20 deletions(-) diff --git a/src/synthetic-homotopy-theory/composition-cospans.lagda.md b/src/synthetic-homotopy-theory/composition-cospans.lagda.md index 48f76fd478f..d24699e3082 100644 --- a/src/synthetic-homotopy-theory/composition-cospans.lagda.md +++ b/src/synthetic-homotopy-theory/composition-cospans.lagda.md @@ -7,19 +7,8 @@ module synthetic-homotopy-theory.composition-cospans where
Imports ```agda -open import foundation.commuting-triangles-of-maps open import foundation.cospans open import foundation.dependent-pair-types -open import foundation.equivalences -open import foundation.equivalences-arrows -open import foundation.equivalences-cospans -open import foundation.homotopies -open import foundation.identity-types -open import foundation.morphisms-arrows -open import foundation.morphisms-cospans -open import foundation.pullbacks -open import foundation.standard-pullbacks -open import foundation.type-arithmetic-standard-pullbacks open import foundation.universe-levels open import foundation-core.function-types @@ -46,15 +35,15 @@ two cospans by forming the [pushout](synthetic-homotopy-theory.pushouts.md) of the middle [cospan diagram](foundation.cospan-diagrams.md) ```text - C - | - | - ∨ - B ------> T - | | - | | - ∨ ⌜ ∨ - A ------> S ------> ∙ + C + | + | + ∨ + B ------> T + | | + | | + ∨ ⌜ ∨ + A ------> S ------> ∙ ``` giving us a cospan `G ∘ F` from `A` to `C`. From 4bcac627b93960f96774591bc9a881470e24e6da Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 28 Nov 2025 16:34:56 +0000 Subject: [PATCH 08/12] fix --- src/foundation/operations-cospans.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/foundation/operations-cospans.lagda.md b/src/foundation/operations-cospans.lagda.md index 334bb7f3162..9574a13156d 100644 --- a/src/foundation/operations-cospans.lagda.md +++ b/src/foundation/operations-cospans.lagda.md @@ -138,5 +138,5 @@ module _ ## See also -- [Composition of cospans](foundation.composition-cospans.md) +- [Composition of cospans](synthetic-homotopy-theory.composition-cospans.md) - [Opposite cospans](foundation.opposite-cospans.md) From bdf1b1cda76333c538894d51b9056e9c8aa6eaea Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 28 Nov 2025 16:46:35 +0000 Subject: [PATCH 09/12] flesh out definitions morphisms and equivalences of cospans --- src/foundation/equivalences-cospans.lagda.md | 51 +++++++++++++++++-- ...otopies-morphisms-cospan-diagrams.lagda.md | 38 +++++++------- .../morphisms-cospan-diagrams.lagda.md | 20 ++++---- src/foundation/morphisms-cospans.lagda.md | 41 +++++++++++---- 4 files changed, 109 insertions(+), 41 deletions(-) diff --git a/src/foundation/equivalences-cospans.lagda.md b/src/foundation/equivalences-cospans.lagda.md index 2f2dac5bde8..ca494a0f821 100644 --- a/src/foundation/equivalences-cospans.lagda.md +++ b/src/foundation/equivalences-cospans.lagda.md @@ -13,6 +13,7 @@ open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopy-induction open import foundation.morphisms-cospans open import foundation.structure-identity-principle +open import foundation.type-arithmetic-dependent-pair-types open import foundation.univalence open import foundation.universe-levels @@ -44,17 +45,59 @@ both [commute](foundation.commuting-triangles-of-maps.md). ## Definitions +### The predicate of being an equivalence of cospans + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} + (s : cospan l3 A B) (t : cospan l4 A B) + where + + is-equiv-hom-cospan : hom-cospan s t → UU (l3 ⊔ l4) + is-equiv-hom-cospan f = is-equiv (map-hom-cospan s t f) +``` + ### Equivalences of cospans ```agda module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} + (s : cospan l3 A B) (t : cospan l4 A B) where - equiv-cospan : cospan l3 A B → cospan l4 A B → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) - equiv-cospan c d = - Σ ( cospanning-type-cospan c ≃ cospanning-type-cospan d) - ( λ e → coherence-hom-cospan c d (map-equiv e)) + equiv-cospan : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + equiv-cospan = + Σ ( cospanning-type-cospan s ≃ cospanning-type-cospan t) + ( λ e → coherence-hom-cospan s t (map-equiv e)) + + equiv-equiv-cospan : + equiv-cospan → cospanning-type-cospan s ≃ cospanning-type-cospan t + equiv-equiv-cospan = pr1 + + map-equiv-cospan : + equiv-cospan → cospanning-type-cospan s → cospanning-type-cospan t + map-equiv-cospan e = map-equiv (equiv-equiv-cospan e) + + left-triangle-equiv-cospan : + (e : equiv-cospan) → left-coherence-hom-cospan s t (map-equiv-cospan e) + left-triangle-equiv-cospan e = pr1 (pr2 e) + + right-triangle-equiv-cospan : + (e : equiv-cospan) → right-coherence-hom-cospan s t (map-equiv-cospan e) + right-triangle-equiv-cospan e = pr2 (pr2 e) + + hom-equiv-cospan : equiv-cospan → hom-cospan s t + pr1 (hom-equiv-cospan e) = map-equiv-cospan e + pr1 (pr2 (hom-equiv-cospan e)) = left-triangle-equiv-cospan e + pr2 (pr2 (hom-equiv-cospan e)) = right-triangle-equiv-cospan e + + is-equiv-equiv-cospan : + (e : equiv-cospan) → is-equiv-hom-cospan s t (hom-equiv-cospan e) + is-equiv-equiv-cospan e = is-equiv-map-equiv (equiv-equiv-cospan e) + + compute-equiv-cospan : + Σ (hom-cospan s t) (is-equiv-hom-cospan s t) ≃ equiv-cospan + compute-equiv-cospan = equiv-right-swap-Σ ``` ### The identity equivalence of cospans diff --git a/src/foundation/homotopies-morphisms-cospan-diagrams.lagda.md b/src/foundation/homotopies-morphisms-cospan-diagrams.lagda.md index 0b4e7d6bb55..6eae5c3328a 100644 --- a/src/foundation/homotopies-morphisms-cospan-diagrams.lagda.md +++ b/src/foundation/homotopies-morphisms-cospan-diagrams.lagda.md @@ -69,8 +69,8 @@ module _ left-square-coherence-htpy-hom-cospan-diagram : (h h' : hom-cospan-diagram 𝒮 𝒯) → - left-map-hom-cospan-diagram 𝒮 𝒯 h ~ - left-map-hom-cospan-diagram 𝒮 𝒯 h' → + map-domain-hom-cospan-diagram 𝒮 𝒯 h ~ + map-domain-hom-cospan-diagram 𝒮 𝒯 h' → cospanning-map-hom-cospan-diagram 𝒮 𝒯 h ~ cospanning-map-hom-cospan-diagram 𝒮 𝒯 h' → UU (l1 ⊔ l3') left-square-coherence-htpy-hom-cospan-diagram h h' L C = @@ -82,8 +82,8 @@ module _ right-square-coherence-htpy-hom-cospan-diagram : (h h' : hom-cospan-diagram 𝒮 𝒯) → - right-map-hom-cospan-diagram 𝒮 𝒯 h ~ - right-map-hom-cospan-diagram 𝒮 𝒯 h' → + map-codomain-hom-cospan-diagram 𝒮 𝒯 h ~ + map-codomain-hom-cospan-diagram 𝒮 𝒯 h' → cospanning-map-hom-cospan-diagram 𝒮 𝒯 h ~ cospanning-map-hom-cospan-diagram 𝒮 𝒯 h' → UU (l2 ⊔ l3') right-square-coherence-htpy-hom-cospan-diagram h h' R C = @@ -95,10 +95,10 @@ module _ coherence-htpy-hom-cospan-diagram : (h h' : hom-cospan-diagram 𝒮 𝒯) → - left-map-hom-cospan-diagram 𝒮 𝒯 h ~ - left-map-hom-cospan-diagram 𝒮 𝒯 h' → - right-map-hom-cospan-diagram 𝒮 𝒯 h ~ - right-map-hom-cospan-diagram 𝒮 𝒯 h' → + map-domain-hom-cospan-diagram 𝒮 𝒯 h ~ + map-domain-hom-cospan-diagram 𝒮 𝒯 h' → + map-codomain-hom-cospan-diagram 𝒮 𝒯 h ~ + map-codomain-hom-cospan-diagram 𝒮 𝒯 h' → cospanning-map-hom-cospan-diagram 𝒮 𝒯 h ~ cospanning-map-hom-cospan-diagram 𝒮 𝒯 h' → UU (l1 ⊔ l2 ⊔ l3') coherence-htpy-hom-cospan-diagram h h' L R C = @@ -108,11 +108,11 @@ module _ htpy-hom-cospan-diagram : (h h' : hom-cospan-diagram 𝒮 𝒯) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l1' ⊔ l2' ⊔ l3') htpy-hom-cospan-diagram h h' = - Σ ( left-map-hom-cospan-diagram 𝒮 𝒯 h ~ - left-map-hom-cospan-diagram 𝒮 𝒯 h') + Σ ( map-domain-hom-cospan-diagram 𝒮 𝒯 h ~ + map-domain-hom-cospan-diagram 𝒮 𝒯 h') ( λ L → - Σ ( right-map-hom-cospan-diagram 𝒮 𝒯 h ~ - right-map-hom-cospan-diagram 𝒮 𝒯 h') + Σ ( map-codomain-hom-cospan-diagram 𝒮 𝒯 h ~ + map-codomain-hom-cospan-diagram 𝒮 𝒯 h') ( λ R → Σ ( cospanning-map-hom-cospan-diagram 𝒮 𝒯 h ~ cospanning-map-hom-cospan-diagram 𝒮 𝒯 h') @@ -127,11 +127,13 @@ module _ where htpy-left-map-htpy-hom-cospan-diagram : - left-map-hom-cospan-diagram 𝒮 𝒯 h ~ left-map-hom-cospan-diagram 𝒮 𝒯 h' + map-domain-hom-cospan-diagram 𝒮 𝒯 h ~ + map-domain-hom-cospan-diagram 𝒮 𝒯 h' htpy-left-map-htpy-hom-cospan-diagram = pr1 H htpy-right-map-htpy-hom-cospan-diagram : - right-map-hom-cospan-diagram 𝒮 𝒯 h ~ right-map-hom-cospan-diagram 𝒮 𝒯 h' + map-codomain-hom-cospan-diagram 𝒮 𝒯 h ~ + map-codomain-hom-cospan-diagram 𝒮 𝒯 h' htpy-right-map-htpy-hom-cospan-diagram = pr1 (pr2 H) htpy-cospanning-map-htpy-hom-cospan-diagram : @@ -183,11 +185,11 @@ module _ (h : hom-cospan-diagram 𝒮 𝒯) → is-torsorial (htpy-hom-cospan-diagram 𝒮 𝒯 h) is-torsorial-htpy-hom-cospan-diagram h = is-torsorial-Eq-structure - ( is-torsorial-htpy (left-map-hom-cospan-diagram 𝒮 𝒯 h)) - ( left-map-hom-cospan-diagram 𝒮 𝒯 h , refl-htpy) + ( is-torsorial-htpy (map-domain-hom-cospan-diagram 𝒮 𝒯 h)) + ( map-domain-hom-cospan-diagram 𝒮 𝒯 h , refl-htpy) ( is-torsorial-Eq-structure - ( is-torsorial-htpy (right-map-hom-cospan-diagram 𝒮 𝒯 h)) - ( right-map-hom-cospan-diagram 𝒮 𝒯 h , refl-htpy) + ( is-torsorial-htpy (map-codomain-hom-cospan-diagram 𝒮 𝒯 h)) + ( map-codomain-hom-cospan-diagram 𝒮 𝒯 h , refl-htpy) ( is-torsorial-Eq-structure ( is-torsorial-htpy (cospanning-map-hom-cospan-diagram 𝒮 𝒯 h)) ( cospanning-map-hom-cospan-diagram 𝒮 𝒯 h , refl-htpy) diff --git a/src/foundation/morphisms-cospan-diagrams.lagda.md b/src/foundation/morphisms-cospan-diagrams.lagda.md index 4e6184a65e2..c57a4d7ba29 100644 --- a/src/foundation/morphisms-cospan-diagrams.lagda.md +++ b/src/foundation/morphisms-cospan-diagrams.lagda.md @@ -58,25 +58,25 @@ module _ (h : hom-cospan-diagram 𝒮 𝒯) where - left-map-hom-cospan-diagram : + map-domain-hom-cospan-diagram : domain-cospan-diagram 𝒮 → domain-cospan-diagram 𝒯 - left-map-hom-cospan-diagram = pr1 h + map-domain-hom-cospan-diagram = pr1 h - right-map-hom-cospan-diagram : + map-codomain-hom-cospan-diagram : codomain-cospan-diagram 𝒮 → codomain-cospan-diagram 𝒯 - right-map-hom-cospan-diagram = pr1 (pr2 h) + map-codomain-hom-cospan-diagram = pr1 (pr2 h) cospanning-map-hom-cospan-diagram : cospanning-type-cospan-diagram 𝒮 → cospanning-type-cospan-diagram 𝒯 cospanning-map-hom-cospan-diagram = pr1 (pr2 (pr2 h)) left-square-hom-cospan-diagram : - left-map-cospan-diagram 𝒯 ∘ left-map-hom-cospan-diagram ~ + left-map-cospan-diagram 𝒯 ∘ map-domain-hom-cospan-diagram ~ cospanning-map-hom-cospan-diagram ∘ left-map-cospan-diagram 𝒮 left-square-hom-cospan-diagram = pr1 (pr2 (pr2 (pr2 h))) right-square-hom-cospan-diagram : - right-map-cospan-diagram 𝒯 ∘ right-map-hom-cospan-diagram ~ + right-map-cospan-diagram 𝒯 ∘ map-codomain-hom-cospan-diagram ~ cospanning-map-hom-cospan-diagram ∘ right-map-cospan-diagram 𝒮 right-square-hom-cospan-diagram = pr2 (pr2 (pr2 (pr2 h))) ``` @@ -134,8 +134,8 @@ module _ ( domain-cospan-diagram 𝒯 , domain-cospan-diagram ℛ , domain-cospan-diagram 𝒮 , - left-map-hom-cospan-diagram 𝒯 𝒮 h , - left-map-hom-cospan-diagram ℛ 𝒮 h') + map-domain-hom-cospan-diagram 𝒯 𝒮 h , + map-domain-hom-cospan-diagram ℛ 𝒮 h') ( codomain-hom-cospan-diagram-rotate h h') hom-cospan-diagram-rotate ( hA , hB , hX , HA , HB) @@ -152,8 +152,8 @@ module _ ( codomain-cospan-diagram 𝒯 , codomain-cospan-diagram ℛ , codomain-cospan-diagram 𝒮 , - right-map-hom-cospan-diagram 𝒯 𝒮 h , - right-map-hom-cospan-diagram ℛ 𝒮 h') + map-codomain-hom-cospan-diagram 𝒯 𝒮 h , + map-codomain-hom-cospan-diagram ℛ 𝒮 h') ( codomain-hom-cospan-diagram-rotate h h') hom-cospan-diagram-rotate' ( hA , hB , hX , HA , HB) diff --git a/src/foundation/morphisms-cospans.lagda.md b/src/foundation/morphisms-cospans.lagda.md index 64fd44b3715..5780e800bbd 100644 --- a/src/foundation/morphisms-cospans.lagda.md +++ b/src/foundation/morphisms-cospans.lagda.md @@ -19,9 +19,9 @@ open import foundation-core.commuting-triangles-of-maps ## Idea -Consider two [cospans](foundation.cospans.md) `c := (X , f , g)` and -`d := (Y , h , k)` from `A` to `B`. A -{{#concept "morphism of cospans" Agda=hom-cospan}} from `c` to `d` consists of a +Consider two [cospans](foundation.cospans.md) `s := (X , f , g)` and +`t := (Y , h , k)` from `A` to `B`. A +{{#concept "morphism of cospans" Agda=hom-cospan}} from `s` to `t` consists of a map `u : X → Y` equipped with [homotopies](foundation-core.homotopies.md) witnessing that the two triangles @@ -43,17 +43,40 @@ witnessing that the two triangles ```agda module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} - (c : cospan l3 A B) (d : cospan l4 A B) + (s : cospan l3 A B) (t : cospan l4 A B) where + left-coherence-hom-cospan : + (cospanning-type-cospan s → cospanning-type-cospan t) → UU (l1 ⊔ l4) + left-coherence-hom-cospan h = + coherence-triangle-maps (left-map-cospan t) h (left-map-cospan s) + + right-coherence-hom-cospan : + (cospanning-type-cospan s → cospanning-type-cospan t) → UU (l2 ⊔ l4) + right-coherence-hom-cospan h = + coherence-triangle-maps (right-map-cospan t) h (right-map-cospan s) + coherence-hom-cospan : - (cospanning-type-cospan c → cospanning-type-cospan d) → UU (l1 ⊔ l2 ⊔ l4) - coherence-hom-cospan h = - ( coherence-triangle-maps (left-map-cospan d) h (left-map-cospan c)) × - ( coherence-triangle-maps (right-map-cospan d) h (right-map-cospan c)) + (cospanning-type-cospan s → cospanning-type-cospan t) → UU (l1 ⊔ l2 ⊔ l4) + coherence-hom-cospan f = + left-coherence-hom-cospan f × right-coherence-hom-cospan f hom-cospan : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) hom-cospan = - Σ ( cospanning-type-cospan c → cospanning-type-cospan d) + Σ ( cospanning-type-cospan s → cospanning-type-cospan t) ( coherence-hom-cospan) + +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} + (s : cospan l3 A B) (t : cospan l4 A B) (f : hom-cospan s t) + where + + map-hom-cospan : cospanning-type-cospan s → cospanning-type-cospan t + map-hom-cospan = pr1 f + + left-triangle-hom-cospan : left-coherence-hom-cospan s t map-hom-cospan + left-triangle-hom-cospan = pr1 (pr2 f) + + right-triangle-hom-cospan : right-coherence-hom-cospan s t map-hom-cospan + right-triangle-hom-cospan = pr2 (pr2 f) ``` From e247dbe721d86396f173de945227c2ba7d0906e3 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 28 Nov 2025 16:55:53 +0000 Subject: [PATCH 10/12] equivalences cospan diagrams (with some todos) --- .../equivalences-cospan-diagrams.lagda.md | 330 ++++++++++++++++++ src/foundation/equivalences-cospans.lagda.md | 32 +- .../equivalences-span-diagrams.lagda.md | 34 +- src/foundation/equivalences-spans.lagda.md | 29 +- 4 files changed, 382 insertions(+), 43 deletions(-) create mode 100644 src/foundation/equivalences-cospan-diagrams.lagda.md diff --git a/src/foundation/equivalences-cospan-diagrams.lagda.md b/src/foundation/equivalences-cospan-diagrams.lagda.md new file mode 100644 index 00000000000..a1d5ad52a55 --- /dev/null +++ b/src/foundation/equivalences-cospan-diagrams.lagda.md @@ -0,0 +1,330 @@ +# Equivalences of cospan diagrams + +```agda +module foundation.equivalences-cospan-diagrams where +``` + +
Imports + +```agda +open import foundation.cartesian-product-types +open import foundation.cospan-diagrams +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.equivalences-arrows +open import foundation.equivalences-cospans +open import foundation.fundamental-theorem-of-identity-types +open import foundation.morphisms-cospan-diagrams +open import foundation.morphisms-cospans +open import foundation.operations-cospans +open import foundation.propositions +open import foundation.structure-identity-principle +open import foundation.type-arithmetic-dependent-pair-types +open import foundation.univalence +open import foundation.universe-levels + +open import foundation-core.commuting-squares-of-maps +open import foundation-core.functoriality-dependent-pair-types +open import foundation-core.identity-types +open import foundation-core.torsorial-type-families +``` + +
+ +## Idea + +An {{#concept "equivalence of cospan diagrams" Agda=equiv-cospan-diagram}} from +a [cospan diagram](foundation.cospan-diagrams.md) `A -f-> S <-g- B` to a cospan +diagram `C -h-> T <-k- D` consists of +[equivalences](foundation-core.equivalences.md) `u : A ≃ C`, `v : B ≃ D`, and +`w : S ≃ T` [equipped](foundation.structure.md) with two +[homotopies](foundation-core.homotopies.md) witnessing that the diagram + +```text + f g + A ------> S <------ B + | | | + u | | w | v + ∨ ∨ ∨ + C ------> T <------ D + h k +``` + +[commutes](foundation-core.commuting-squares-of-maps.md). + +## Definitions + +### The predicate of being an equivalence of cospan diagrams + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + (𝒮 : cospan-diagram l1 l2 l3) (𝒯 : cospan-diagram l4 l5 l6) + (f : hom-cospan-diagram 𝒮 𝒯) + where + + is-equiv-prop-hom-cospan-diagram : Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6) + is-equiv-prop-hom-cospan-diagram = + product-Prop + ( is-equiv-Prop (map-domain-hom-cospan-diagram 𝒮 𝒯 f)) + ( product-Prop + ( is-equiv-Prop (map-codomain-hom-cospan-diagram 𝒮 𝒯 f)) + ( is-equiv-Prop (cospanning-map-hom-cospan-diagram 𝒮 𝒯 f))) + + is-equiv-hom-cospan-diagram : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6) + is-equiv-hom-cospan-diagram = type-Prop is-equiv-prop-hom-cospan-diagram + + is-prop-is-equiv-hom-cospan-diagram : is-prop is-equiv-hom-cospan-diagram + is-prop-is-equiv-hom-cospan-diagram = + is-prop-type-Prop is-equiv-prop-hom-cospan-diagram +``` + +### Equivalences of cospan diagrams + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + (𝒮 : cospan-diagram l1 l2 l3) (𝒯 : cospan-diagram l4 l5 l6) + where + + equiv-cospan-diagram : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6) + equiv-cospan-diagram = + Σ ( domain-cospan-diagram 𝒮 ≃ domain-cospan-diagram 𝒯) + ( λ e → + Σ ( codomain-cospan-diagram 𝒮 ≃ codomain-cospan-diagram 𝒯) + ( λ f → + equiv-cospan + ( cospan-cospan-diagram 𝒮) + ( concat-cospan + ( cospan-cospan-diagram 𝒯) + ( map-equiv e) + ( map-equiv f)))) + + module _ + (e : equiv-cospan-diagram) + where + + equiv-domain-equiv-cospan-diagram : + domain-cospan-diagram 𝒮 ≃ domain-cospan-diagram 𝒯 + equiv-domain-equiv-cospan-diagram = pr1 e + + map-domain-equiv-cospan-diagram : + domain-cospan-diagram 𝒮 → domain-cospan-diagram 𝒯 + map-domain-equiv-cospan-diagram = + map-equiv equiv-domain-equiv-cospan-diagram + + is-equiv-map-domain-equiv-cospan-diagram : + is-equiv map-domain-equiv-cospan-diagram + is-equiv-map-domain-equiv-cospan-diagram = + is-equiv-map-equiv equiv-domain-equiv-cospan-diagram + + equiv-codomain-equiv-cospan-diagram : + codomain-cospan-diagram 𝒮 ≃ codomain-cospan-diagram 𝒯 + equiv-codomain-equiv-cospan-diagram = pr1 (pr2 e) + + map-codomain-equiv-cospan-diagram : + codomain-cospan-diagram 𝒮 → codomain-cospan-diagram 𝒯 + map-codomain-equiv-cospan-diagram = + map-equiv equiv-codomain-equiv-cospan-diagram + + is-equiv-map-codomain-equiv-cospan-diagram : + is-equiv map-codomain-equiv-cospan-diagram + is-equiv-map-codomain-equiv-cospan-diagram = + is-equiv-map-equiv equiv-codomain-equiv-cospan-diagram + + equiv-cospan-equiv-cospan-diagram : + equiv-cospan + ( cospan-cospan-diagram 𝒮) + ( concat-cospan + ( cospan-cospan-diagram 𝒯) + ( map-domain-equiv-cospan-diagram) + ( map-codomain-equiv-cospan-diagram)) + equiv-cospan-equiv-cospan-diagram = + pr2 (pr2 e) + + cospanning-equiv-equiv-cospan-diagram : + cospanning-type-cospan-diagram 𝒮 ≃ cospanning-type-cospan-diagram 𝒯 + cospanning-equiv-equiv-cospan-diagram = + equiv-equiv-cospan + ( cospan-cospan-diagram 𝒮) + ( concat-cospan + ( cospan-cospan-diagram 𝒯) + ( map-domain-equiv-cospan-diagram) + ( map-codomain-equiv-cospan-diagram)) + ( equiv-cospan-equiv-cospan-diagram) + + cospanning-map-equiv-cospan-diagram : + cospanning-type-cospan-diagram 𝒮 → cospanning-type-cospan-diagram 𝒯 + cospanning-map-equiv-cospan-diagram = + map-equiv-cospan + ( cospan-cospan-diagram 𝒮) + ( concat-cospan + ( cospan-cospan-diagram 𝒯) + ( map-domain-equiv-cospan-diagram) + ( map-codomain-equiv-cospan-diagram)) + ( equiv-cospan-equiv-cospan-diagram) + + is-equiv-cospanning-map-equiv-cospan-diagram : + is-equiv cospanning-map-equiv-cospan-diagram + is-equiv-cospanning-map-equiv-cospan-diagram = + is-equiv-equiv-cospan + ( cospan-cospan-diagram 𝒮) + ( concat-cospan + ( cospan-cospan-diagram 𝒯) + ( map-domain-equiv-cospan-diagram) + ( map-codomain-equiv-cospan-diagram)) + ( equiv-cospan-equiv-cospan-diagram) + + -- left-square-equiv-cospan-diagram : + -- coherence-square-maps + -- ( cospanning-map-equiv-cospan-diagram) + -- ( left-map-cospan-diagram 𝒮) + -- ( left-map-cospan-diagram 𝒯) + -- ( map-domain-equiv-cospan-diagram) + -- left-square-equiv-cospan-diagram = + -- left-triangle-equiv-cospan + -- ( concat-cospan + -- ( cospan-cospan-diagram 𝒮) + -- ( map-domain-equiv-cospan-diagram) + -- ( map-codomain-equiv-cospan-diagram)) + -- ( cospan-cospan-diagram 𝒯) + -- ( equiv-cospan-equiv-cospan-diagram) + + -- equiv-left-arrow-equiv-cospan-diagram : + -- equiv-arrow (left-map-cospan-diagram 𝒮) (left-map-cospan-diagram 𝒯) + -- pr1 equiv-left-arrow-equiv-cospan-diagram = + -- cospanning-equiv-equiv-cospan-diagram + -- pr1 (pr2 equiv-left-arrow-equiv-cospan-diagram) = + -- equiv-domain-equiv-cospan-diagram + -- pr2 (pr2 equiv-left-arrow-equiv-cospan-diagram) = + -- left-square-equiv-cospan-diagram + + -- right-square-equiv-cospan-diagram : + -- coherence-square-maps + -- ( cospanning-map-equiv-cospan-diagram) + -- ( right-map-cospan-diagram 𝒮) + -- ( right-map-cospan-diagram 𝒯) + -- ( map-codomain-equiv-cospan-diagram) + -- right-square-equiv-cospan-diagram = + -- right-triangle-equiv-cospan + -- ( concat-cospan + -- ( cospan-cospan-diagram 𝒮) + -- ( map-domain-equiv-cospan-diagram) + -- ( map-codomain-equiv-cospan-diagram)) + -- ( cospan-cospan-diagram 𝒯) + -- ( equiv-cospan-equiv-cospan-diagram) + + -- equiv-right-arrow-equiv-cospan-diagram : + -- equiv-arrow (right-map-cospan-diagram 𝒮) (right-map-cospan-diagram 𝒯) + -- pr1 equiv-right-arrow-equiv-cospan-diagram = + -- cospanning-equiv-equiv-cospan-diagram + -- pr1 (pr2 equiv-right-arrow-equiv-cospan-diagram) = + -- equiv-codomain-equiv-cospan-diagram + -- pr2 (pr2 equiv-right-arrow-equiv-cospan-diagram) = + -- right-square-equiv-cospan-diagram + + -- hom-cospan-equiv-cospan-diagram : + -- hom-cospan + -- ( concat-cospan + -- ( cospan-cospan-diagram 𝒮) + -- ( map-domain-equiv-cospan-diagram) + -- ( map-codomain-equiv-cospan-diagram)) + -- ( cospan-cospan-diagram 𝒯) + -- hom-cospan-equiv-cospan-diagram = + -- hom-equiv-cospan + -- ( concat-cospan + -- ( cospan-cospan-diagram 𝒮) + -- ( map-domain-equiv-cospan-diagram) + -- ( map-codomain-equiv-cospan-diagram)) + -- ( cospan-cospan-diagram 𝒯) + -- ( equiv-cospan-equiv-cospan-diagram) + + -- hom-equiv-cospan-diagram : hom-cospan-diagram 𝒮 𝒯 + -- pr1 hom-equiv-cospan-diagram = map-domain-equiv-cospan-diagram + -- pr1 (pr2 hom-equiv-cospan-diagram) = map-codomain-equiv-cospan-diagram + -- pr2 (pr2 hom-equiv-cospan-diagram) = hom-cospan-equiv-cospan-diagram + + -- is-equiv-equiv-cospan-diagram : + -- is-equiv-hom-cospan-diagram 𝒮 𝒯 hom-equiv-cospan-diagram + -- pr1 is-equiv-equiv-cospan-diagram = + -- is-equiv-map-domain-equiv-cospan-diagram + -- pr1 (pr2 is-equiv-equiv-cospan-diagram) = + -- is-equiv-map-codomain-equiv-cospan-diagram + -- pr2 (pr2 is-equiv-equiv-cospan-diagram) = + -- is-equiv-cospanning-map-equiv-cospan-diagram + + -- compute-equiv-cospan-diagram : + -- Σ (hom-cospan-diagram 𝒮 𝒯) (is-equiv-hom-cospan-diagram 𝒮 𝒯) ≃ + -- equiv-cospan-diagram + -- compute-equiv-cospan-diagram = + -- ( equiv-tot + -- ( λ e → + -- ( equiv-tot + -- ( λ f → + -- compute-equiv-cospan + -- ( concat-cospan + -- ( cospan-cospan-diagram 𝒮) + -- ( map-equiv e) + -- ( map-equiv f)) + -- ( cospan-cospan-diagram 𝒯))) ∘e + -- ( interchange-Σ-Σ _))) ∘e + -- ( interchange-Σ-Σ _) +``` + +### The identity equivalence of cospan diagrams + +```agda +module _ + {l1 l2 l3 : Level} (𝒮 : cospan-diagram l1 l2 l3) + where + + id-equiv-cospan-diagram : equiv-cospan-diagram 𝒮 𝒮 + pr1 id-equiv-cospan-diagram = id-equiv + pr1 (pr2 id-equiv-cospan-diagram) = id-equiv + pr2 (pr2 id-equiv-cospan-diagram) = id-equiv-cospan (cospan-cospan-diagram 𝒮) +``` + +## Properties + +### Extensionality of cospan diagrams + +Equality of cospan diagrams is equivalent to equivalences of cospan diagrams. + +```agda +module _ + {l1 l2 l3 : Level} (𝒮 : cospan-diagram l1 l2 l3) + where + + equiv-eq-cospan-diagram : + (𝒯 : cospan-diagram l1 l2 l3) → 𝒮 ＝ 𝒯 → equiv-cospan-diagram 𝒮 𝒯 + equiv-eq-cospan-diagram 𝒯 refl = id-equiv-cospan-diagram 𝒮 + + abstract + is-torsorial-equiv-cospan-diagram : + is-torsorial (equiv-cospan-diagram {l1} {l2} {l3} {l1} {l2} {l3} 𝒮) + is-torsorial-equiv-cospan-diagram = + is-torsorial-Eq-structure + ( is-torsorial-equiv (domain-cospan-diagram 𝒮)) + ( domain-cospan-diagram 𝒮 , id-equiv) + ( is-torsorial-Eq-structure + ( is-torsorial-equiv (codomain-cospan-diagram 𝒮)) + ( codomain-cospan-diagram 𝒮 , id-equiv) + ( is-torsorial-equiv-cospan (cospan-cospan-diagram 𝒮))) + + abstract + is-equiv-equiv-eq-cospan-diagram : + (𝒯 : cospan-diagram l1 l2 l3) → is-equiv (equiv-eq-cospan-diagram 𝒯) + is-equiv-equiv-eq-cospan-diagram = + fundamental-theorem-id + ( is-torsorial-equiv-cospan-diagram) + ( equiv-eq-cospan-diagram) + + extensionality-cospan-diagram : + (𝒯 : cospan-diagram l1 l2 l3) → (𝒮 ＝ 𝒯) ≃ equiv-cospan-diagram 𝒮 𝒯 + pr1 (extensionality-cospan-diagram 𝒯) = equiv-eq-cospan-diagram 𝒯 + pr2 (extensionality-cospan-diagram 𝒯) = is-equiv-equiv-eq-cospan-diagram 𝒯 + + eq-equiv-cospan-diagram : + (𝒯 : cospan-diagram l1 l2 l3) → equiv-cospan-diagram 𝒮 𝒯 → 𝒮 ＝ 𝒯 + eq-equiv-cospan-diagram 𝒯 = map-inv-equiv (extensionality-cospan-diagram 𝒯) +``` diff --git a/src/foundation/equivalences-cospans.lagda.md b/src/foundation/equivalences-cospans.lagda.md index ca494a0f821..769fa13bfab 100644 --- a/src/foundation/equivalences-cospans.lagda.md +++ b/src/foundation/equivalences-cospans.lagda.md @@ -125,21 +125,23 @@ module _ equiv-eq-cospan : (c d : cospan l3 A B) → c ＝ d → equiv-cospan c d equiv-eq-cospan c .c refl = id-equiv-cospan c - is-torsorial-equiv-cospan : - (c : cospan l3 A B) → is-torsorial (equiv-cospan c) - is-torsorial-equiv-cospan c = - is-torsorial-Eq-structure - ( is-torsorial-equiv (pr1 c)) - ( cospanning-type-cospan c , id-equiv) - ( is-torsorial-Eq-structure - ( is-torsorial-htpy' (left-map-cospan c)) - ( left-map-cospan c , refl-htpy) - ( is-torsorial-htpy' (right-map-cospan c))) - - is-equiv-equiv-eq-cospan : - (c d : cospan l3 A B) → is-equiv (equiv-eq-cospan c d) - is-equiv-equiv-eq-cospan c = - fundamental-theorem-id (is-torsorial-equiv-cospan c) (equiv-eq-cospan c) + abstract + is-torsorial-equiv-cospan : + (c : cospan l3 A B) → is-torsorial (equiv-cospan {l1} {l2} {l3} {l3} c) + is-torsorial-equiv-cospan c = + is-torsorial-Eq-structure + ( is-torsorial-equiv (pr1 c)) + ( cospanning-type-cospan c , id-equiv) + ( is-torsorial-Eq-structure + ( is-torsorial-htpy' (left-map-cospan c)) + ( left-map-cospan c , refl-htpy) + ( is-torsorial-htpy' (right-map-cospan c))) + + abstract + is-equiv-equiv-eq-cospan : + (c d : cospan l3 A B) → is-equiv (equiv-eq-cospan c d) + is-equiv-equiv-eq-cospan c = + fundamental-theorem-id (is-torsorial-equiv-cospan c) (equiv-eq-cospan c) extensionality-cospan : (c d : cospan l3 A B) → (c ＝ d) ≃ (equiv-cospan c d) diff --git a/src/foundation/equivalences-span-diagrams.lagda.md b/src/foundation/equivalences-span-diagrams.lagda.md index 92238d6cff9..ca8b7fe1174 100644 --- a/src/foundation/equivalences-span-diagrams.lagda.md +++ b/src/foundation/equivalences-span-diagrams.lagda.md @@ -294,21 +294,25 @@ module _ (𝒯 : span-diagram l1 l2 l3) → 𝒮 ＝ 𝒯 → equiv-span-diagram 𝒮 𝒯 equiv-eq-span-diagram 𝒯 refl = id-equiv-span-diagram 𝒮 - is-torsorial-equiv-span-diagram : - is-torsorial (equiv-span-diagram 𝒮) - is-torsorial-equiv-span-diagram = - is-torsorial-Eq-structure - ( is-torsorial-equiv (domain-span-diagram 𝒮)) - ( domain-span-diagram 𝒮 , id-equiv) - ( is-torsorial-Eq-structure - ( is-torsorial-equiv (codomain-span-diagram 𝒮)) - ( codomain-span-diagram 𝒮 , id-equiv) - ( is-torsorial-equiv-span (span-span-diagram 𝒮))) - - is-equiv-equiv-eq-span-diagram : - (𝒯 : span-diagram l1 l2 l3) → is-equiv (equiv-eq-span-diagram 𝒯) - is-equiv-equiv-eq-span-diagram = - fundamental-theorem-id is-torsorial-equiv-span-diagram equiv-eq-span-diagram + abstract + is-torsorial-equiv-span-diagram : + is-torsorial (equiv-span-diagram {l1} {l2} {l3} {l1} {l2} {l3} 𝒮) + is-torsorial-equiv-span-diagram = + is-torsorial-Eq-structure + ( is-torsorial-equiv (domain-span-diagram 𝒮)) + ( domain-span-diagram 𝒮 , id-equiv) + ( is-torsorial-Eq-structure + ( is-torsorial-equiv (codomain-span-diagram 𝒮)) + ( codomain-span-diagram 𝒮 , id-equiv) + ( is-torsorial-equiv-span (span-span-diagram 𝒮))) + + abstract + is-equiv-equiv-eq-span-diagram : + (𝒯 : span-diagram l1 l2 l3) → is-equiv (equiv-eq-span-diagram 𝒯) + is-equiv-equiv-eq-span-diagram = + fundamental-theorem-id + ( is-torsorial-equiv-span-diagram) + ( equiv-eq-span-diagram) extensionality-span-diagram : (𝒯 : span-diagram l1 l2 l3) → (𝒮 ＝ 𝒯) ≃ equiv-span-diagram 𝒮 𝒯 diff --git a/src/foundation/equivalences-spans.lagda.md b/src/foundation/equivalences-spans.lagda.md index 4e804c318a2..b712f62b6f9 100644 --- a/src/foundation/equivalences-spans.lagda.md +++ b/src/foundation/equivalences-spans.lagda.md @@ -148,19 +148,22 @@ module _ equiv-eq-span : (s t : span l3 A B) → s ＝ t → equiv-span s t equiv-eq-span s .s refl = id-equiv-span s - is-torsorial-equiv-span : (s : span l3 A B) → is-torsorial (equiv-span s) - is-torsorial-equiv-span s = - is-torsorial-Eq-structure - ( is-torsorial-equiv (spanning-type-span s)) - ( spanning-type-span s , id-equiv) - ( is-torsorial-Eq-structure - ( is-torsorial-htpy (left-map-span s)) - ( left-map-span s , refl-htpy) - ( is-torsorial-htpy (right-map-span s))) - - is-equiv-equiv-eq-span : (c d : span l3 A B) → is-equiv (equiv-eq-span c d) - is-equiv-equiv-eq-span c = - fundamental-theorem-id (is-torsorial-equiv-span c) (equiv-eq-span c) + abstract + is-torsorial-equiv-span : + (s : span l3 A B) → is-torsorial (equiv-span {l1} {l2} {l3} {l3} s) + is-torsorial-equiv-span s = + is-torsorial-Eq-structure + ( is-torsorial-equiv (spanning-type-span s)) + ( spanning-type-span s , id-equiv) + ( is-torsorial-Eq-structure + ( is-torsorial-htpy (left-map-span s)) + ( left-map-span s , refl-htpy) + ( is-torsorial-htpy (right-map-span s))) + + abstract + is-equiv-equiv-eq-span : (c d : span l3 A B) → is-equiv (equiv-eq-span c d) + is-equiv-equiv-eq-span c = + fundamental-theorem-id (is-torsorial-equiv-span c) (equiv-eq-span c) extensionality-span : (c d : span l3 A B) → (c ＝ d) ≃ (equiv-span c d) pr1 (extensionality-span c d) = equiv-eq-span c d From 357ffadab031455eb13d7642f224e1d38d39db5b Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 28 Nov 2025 16:56:23 +0000 Subject: [PATCH 11/12] pre-commit --- src/foundation.lagda.md | 1 + 1 file changed, 1 insertion(+) diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index 40e20ba6dce..e110bfd40fe 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -180,6 +180,7 @@ open import foundation.equivalence-injective-type-families public open import foundation.equivalence-relations public open import foundation.equivalences public open import foundation.equivalences-arrows public +open import foundation.equivalences-cospan-diagrams public open import foundation.equivalences-cospans public open import foundation.equivalences-double-arrows public open import foundation.equivalences-inverse-sequential-diagrams public From 64ca64be967e68da77f309b252ddccfc2454106b Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 29 Nov 2025 10:39:24 +0000 Subject: [PATCH 12/12] finish --- .../equivalences-cospan-diagrams.lagda.md | 189 +++++++++--------- .../morphisms-cospan-diagrams.lagda.md | 31 +++ 2 files changed, 126 insertions(+), 94 deletions(-) diff --git a/src/foundation/equivalences-cospan-diagrams.lagda.md b/src/foundation/equivalences-cospan-diagrams.lagda.md index a1d5ad52a55..42bb459a494 100644 --- a/src/foundation/equivalences-cospan-diagrams.lagda.md +++ b/src/foundation/equivalences-cospan-diagrams.lagda.md @@ -14,6 +14,7 @@ open import foundation.equivalences open import foundation.equivalences-arrows open import foundation.equivalences-cospans open import foundation.fundamental-theorem-of-identity-types +open import foundation.homotopies open import foundation.morphisms-cospan-diagrams open import foundation.morphisms-cospans open import foundation.operations-cospans @@ -175,100 +176,100 @@ module _ ( map-codomain-equiv-cospan-diagram)) ( equiv-cospan-equiv-cospan-diagram) - -- left-square-equiv-cospan-diagram : - -- coherence-square-maps - -- ( cospanning-map-equiv-cospan-diagram) - -- ( left-map-cospan-diagram 𝒮) - -- ( left-map-cospan-diagram 𝒯) - -- ( map-domain-equiv-cospan-diagram) - -- left-square-equiv-cospan-diagram = - -- left-triangle-equiv-cospan - -- ( concat-cospan - -- ( cospan-cospan-diagram 𝒮) - -- ( map-domain-equiv-cospan-diagram) - -- ( map-codomain-equiv-cospan-diagram)) - -- ( cospan-cospan-diagram 𝒯) - -- ( equiv-cospan-equiv-cospan-diagram) - - -- equiv-left-arrow-equiv-cospan-diagram : - -- equiv-arrow (left-map-cospan-diagram 𝒮) (left-map-cospan-diagram 𝒯) - -- pr1 equiv-left-arrow-equiv-cospan-diagram = - -- cospanning-equiv-equiv-cospan-diagram - -- pr1 (pr2 equiv-left-arrow-equiv-cospan-diagram) = - -- equiv-domain-equiv-cospan-diagram - -- pr2 (pr2 equiv-left-arrow-equiv-cospan-diagram) = - -- left-square-equiv-cospan-diagram - - -- right-square-equiv-cospan-diagram : - -- coherence-square-maps - -- ( cospanning-map-equiv-cospan-diagram) - -- ( right-map-cospan-diagram 𝒮) - -- ( right-map-cospan-diagram 𝒯) - -- ( map-codomain-equiv-cospan-diagram) - -- right-square-equiv-cospan-diagram = - -- right-triangle-equiv-cospan - -- ( concat-cospan - -- ( cospan-cospan-diagram 𝒮) - -- ( map-domain-equiv-cospan-diagram) - -- ( map-codomain-equiv-cospan-diagram)) - -- ( cospan-cospan-diagram 𝒯) - -- ( equiv-cospan-equiv-cospan-diagram) - - -- equiv-right-arrow-equiv-cospan-diagram : - -- equiv-arrow (right-map-cospan-diagram 𝒮) (right-map-cospan-diagram 𝒯) - -- pr1 equiv-right-arrow-equiv-cospan-diagram = - -- cospanning-equiv-equiv-cospan-diagram - -- pr1 (pr2 equiv-right-arrow-equiv-cospan-diagram) = - -- equiv-codomain-equiv-cospan-diagram - -- pr2 (pr2 equiv-right-arrow-equiv-cospan-diagram) = - -- right-square-equiv-cospan-diagram - - -- hom-cospan-equiv-cospan-diagram : - -- hom-cospan - -- ( concat-cospan - -- ( cospan-cospan-diagram 𝒮) - -- ( map-domain-equiv-cospan-diagram) - -- ( map-codomain-equiv-cospan-diagram)) - -- ( cospan-cospan-diagram 𝒯) - -- hom-cospan-equiv-cospan-diagram = - -- hom-equiv-cospan - -- ( concat-cospan - -- ( cospan-cospan-diagram 𝒮) - -- ( map-domain-equiv-cospan-diagram) - -- ( map-codomain-equiv-cospan-diagram)) - -- ( cospan-cospan-diagram 𝒯) - -- ( equiv-cospan-equiv-cospan-diagram) - - -- hom-equiv-cospan-diagram : hom-cospan-diagram 𝒮 𝒯 - -- pr1 hom-equiv-cospan-diagram = map-domain-equiv-cospan-diagram - -- pr1 (pr2 hom-equiv-cospan-diagram) = map-codomain-equiv-cospan-diagram - -- pr2 (pr2 hom-equiv-cospan-diagram) = hom-cospan-equiv-cospan-diagram - - -- is-equiv-equiv-cospan-diagram : - -- is-equiv-hom-cospan-diagram 𝒮 𝒯 hom-equiv-cospan-diagram - -- pr1 is-equiv-equiv-cospan-diagram = - -- is-equiv-map-domain-equiv-cospan-diagram - -- pr1 (pr2 is-equiv-equiv-cospan-diagram) = - -- is-equiv-map-codomain-equiv-cospan-diagram - -- pr2 (pr2 is-equiv-equiv-cospan-diagram) = - -- is-equiv-cospanning-map-equiv-cospan-diagram - - -- compute-equiv-cospan-diagram : - -- Σ (hom-cospan-diagram 𝒮 𝒯) (is-equiv-hom-cospan-diagram 𝒮 𝒯) ≃ - -- equiv-cospan-diagram - -- compute-equiv-cospan-diagram = - -- ( equiv-tot - -- ( λ e → - -- ( equiv-tot - -- ( λ f → - -- compute-equiv-cospan - -- ( concat-cospan - -- ( cospan-cospan-diagram 𝒮) - -- ( map-equiv e) - -- ( map-equiv f)) - -- ( cospan-cospan-diagram 𝒯))) ∘e - -- ( interchange-Σ-Σ _))) ∘e - -- ( interchange-Σ-Σ _) + left-square-equiv-cospan-diagram : + coherence-square-maps + ( left-map-cospan-diagram 𝒮) + ( map-domain-equiv-cospan-diagram) + ( cospanning-map-equiv-cospan-diagram) + ( left-map-cospan-diagram 𝒯) + left-square-equiv-cospan-diagram = + left-triangle-equiv-cospan + ( cospan-cospan-diagram 𝒮) + ( concat-cospan + ( cospan-cospan-diagram 𝒯) + ( map-domain-equiv-cospan-diagram) + ( map-codomain-equiv-cospan-diagram)) + ( equiv-cospan-equiv-cospan-diagram) + + equiv-left-arrow-equiv-cospan-diagram : + equiv-arrow (left-map-cospan-diagram 𝒮) (left-map-cospan-diagram 𝒯) + pr1 equiv-left-arrow-equiv-cospan-diagram = + equiv-domain-equiv-cospan-diagram + pr1 (pr2 equiv-left-arrow-equiv-cospan-diagram) = + cospanning-equiv-equiv-cospan-diagram + pr2 (pr2 equiv-left-arrow-equiv-cospan-diagram) = + inv-htpy left-square-equiv-cospan-diagram + + right-square-equiv-cospan-diagram : + coherence-square-maps + ( right-map-cospan-diagram 𝒮) + ( map-codomain-equiv-cospan-diagram) + ( cospanning-map-equiv-cospan-diagram) + ( right-map-cospan-diagram 𝒯) + right-square-equiv-cospan-diagram = + right-triangle-equiv-cospan + ( cospan-cospan-diagram 𝒮) + ( concat-cospan + ( cospan-cospan-diagram 𝒯) + ( map-domain-equiv-cospan-diagram) + ( map-codomain-equiv-cospan-diagram)) + ( equiv-cospan-equiv-cospan-diagram) + + equiv-right-arrow-equiv-cospan-diagram : + equiv-arrow (right-map-cospan-diagram 𝒮) (right-map-cospan-diagram 𝒯) + pr1 equiv-right-arrow-equiv-cospan-diagram = + equiv-codomain-equiv-cospan-diagram + pr1 (pr2 equiv-right-arrow-equiv-cospan-diagram) = + cospanning-equiv-equiv-cospan-diagram + pr2 (pr2 equiv-right-arrow-equiv-cospan-diagram) = + inv-htpy right-square-equiv-cospan-diagram + + hom-cospan-equiv-cospan-diagram : + hom-cospan + ( cospan-cospan-diagram 𝒮) + ( concat-cospan + ( cospan-cospan-diagram 𝒯) + ( map-domain-equiv-cospan-diagram) + ( map-codomain-equiv-cospan-diagram)) + hom-cospan-equiv-cospan-diagram = + hom-equiv-cospan + ( cospan-cospan-diagram 𝒮) + ( concat-cospan + ( cospan-cospan-diagram 𝒯) + ( map-domain-equiv-cospan-diagram) + ( map-codomain-equiv-cospan-diagram)) + ( equiv-cospan-equiv-cospan-diagram) + + hom-equiv-cospan-diagram : hom-cospan-diagram 𝒮 𝒯 + pr1 hom-equiv-cospan-diagram = map-domain-equiv-cospan-diagram + pr1 (pr2 hom-equiv-cospan-diagram) = map-codomain-equiv-cospan-diagram + pr2 (pr2 hom-equiv-cospan-diagram) = hom-cospan-equiv-cospan-diagram + + is-equiv-equiv-cospan-diagram : + is-equiv-hom-cospan-diagram 𝒮 𝒯 hom-equiv-cospan-diagram + pr1 is-equiv-equiv-cospan-diagram = + is-equiv-map-domain-equiv-cospan-diagram + pr1 (pr2 is-equiv-equiv-cospan-diagram) = + is-equiv-map-codomain-equiv-cospan-diagram + pr2 (pr2 is-equiv-equiv-cospan-diagram) = + is-equiv-cospanning-map-equiv-cospan-diagram + + compute-equiv-cospan-diagram : + Σ (hom-cospan-diagram 𝒮 𝒯) (is-equiv-hom-cospan-diagram 𝒮 𝒯) ≃ + equiv-cospan-diagram + compute-equiv-cospan-diagram = + ( equiv-tot + ( λ a → + ( equiv-tot + ( λ b → + compute-equiv-cospan + ( cospan-cospan-diagram 𝒮) + ( concat-cospan + ( cospan-cospan-diagram 𝒯) + ( map-equiv a) + ( map-equiv b)))) ∘e + ( interchange-Σ-Σ _))) ∘e + ( interchange-Σ-Σ _) ``` ### The identity equivalence of cospan diagrams diff --git a/src/foundation/morphisms-cospan-diagrams.lagda.md b/src/foundation/morphisms-cospan-diagrams.lagda.md index c57a4d7ba29..2f92052155b 100644 --- a/src/foundation/morphisms-cospan-diagrams.lagda.md +++ b/src/foundation/morphisms-cospan-diagrams.lagda.md @@ -9,6 +9,7 @@ module foundation.morphisms-cospan-diagrams where ```agda open import foundation.cospan-diagrams open import foundation.dependent-pair-types +open import foundation.morphisms-arrows open import foundation.universe-levels open import foundation.whiskering-homotopies-composition @@ -79,6 +80,36 @@ module _ right-map-cospan-diagram 𝒯 ∘ map-codomain-hom-cospan-diagram ~ cospanning-map-hom-cospan-diagram ∘ right-map-cospan-diagram 𝒮 right-square-hom-cospan-diagram = pr2 (pr2 (pr2 (pr2 h))) + + hom-left-arrow-hom-cospan-diagram' : + hom-arrow' (left-map-cospan-diagram 𝒮) (left-map-cospan-diagram 𝒯) + hom-left-arrow-hom-cospan-diagram' = + ( map-domain-hom-cospan-diagram , + cospanning-map-hom-cospan-diagram , + left-square-hom-cospan-diagram) + + hom-right-arrow-hom-cospan-diagram' : + hom-arrow' (right-map-cospan-diagram 𝒮) (right-map-cospan-diagram 𝒯) + hom-right-arrow-hom-cospan-diagram' = + ( map-codomain-hom-cospan-diagram , + cospanning-map-hom-cospan-diagram , + right-square-hom-cospan-diagram) + + hom-left-arrow-hom-cospan-diagram : + hom-arrow (left-map-cospan-diagram 𝒮) (left-map-cospan-diagram 𝒯) + hom-left-arrow-hom-cospan-diagram = + hom-arrow-hom-arrow' + ( left-map-cospan-diagram 𝒮) + ( left-map-cospan-diagram 𝒯) + ( hom-left-arrow-hom-cospan-diagram') + + hom-right-arrow-hom-cospan-diagram : + hom-arrow (right-map-cospan-diagram 𝒮) (right-map-cospan-diagram 𝒯) + hom-right-arrow-hom-cospan-diagram = + hom-arrow-hom-arrow' + ( right-map-cospan-diagram 𝒮) + ( right-map-cospan-diagram 𝒯) + ( hom-right-arrow-hom-cospan-diagram') ``` ### Identity morphisms of cospan diagrams