Cospans of types

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-07-26.
Last modified on 2024-10-27.

module foundation.cospans where

open import foundation.dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopy-induction
open import foundation.structure-identity-principle
open import foundation.univalence
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.commuting-triangles-of-maps
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.torsorial-type-families

Idea

A cospan^¶ from A to B consists of a type X and maps f : A → X and g : B → X, as indicated in the diagram

      f         g
  A -----> X <----- B

We disambiguate between cospans and cospan diagrams. We consider a cospan from A to B a morphism from A to B in the category of types and cospans between them, whereas we consider cospan diagrams to be objects in the category of diagrams of types of the form * <---- * ----> *. Conceptually there is a subtle, but important distinction between cospans and cospan diagrams. Cospan diagrams are more suitable for functorial operations that take “cospans” as input, but for which the functorial action takes a natural transformation, i.e., a morphism of cospan diagrams, as input. Examples of this kind include pullbacks.

Definitions

Cospans

cospan :
  {l1 l2 : Level} (l : Level) (A : UU l1) (B : UU l2) →
  UU (l1 ⊔ l2 ⊔ lsuc l)
cospan l A B = Σ (UU l) (λ X → (A → X) × (B → X))

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

  left-map-cospan : A → codomain-cospan
  left-map-cospan = pr1 (pr2 c)

  right-map-cospan : B → codomain-cospan
  right-map-cospan = pr2 (pr2 c)

The identity cospan

id-cospan : {l : Level} (A : UU l) → cospan l A A
id-cospan A = (A , id , id)

The swapping operation on cospans

swap-cospan :
  {l1 l2 : Level} {l : Level} {A : UU l1} {B : UU l2} →
  cospan l A B → cospan l B A
swap-cospan (C , f , g) = (C , g , f)

See also

• The formal dual of cospans is spans.
• Pullbacks are limits of cospan diagrams.

Table of files about pullbacks

The following table lists files that are about pullbacks as a general concept.

Recent changes

• 2024-10-27. Fredrik Bakke. Functoriality of morphisms of arrows (#1130).
• 2024-01-28. Egbert Rijke. Span diagrams (#1007).
• 2024-01-25. Fredrik Bakke. Basic properties of orthogonal maps (#979).
• 2024-01-11. Fredrik Bakke. Make type family implicit for is-torsorial-Eq-structure and is-torsorial-Eq-Π (#995).
• 2023-11-24. Egbert Rijke. Refactor precomposition (#937).