Cospans of types

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

Created on 2022-07-26.
Last modified on 2024-01-28.

module foundation.cospans where

Imports
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)


See also

Table of files about pullbacks

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

ConceptFile
Cospan diagramsfoundation.cospans
Morphisms of cospan diagramsfoundation.morphisms-cospans
Cones over cospan diagramsfoundation.cones-over-cospan-diagrams
The universal property of pullbacks (foundation-core)foundation-core.universal-property-pullbacks
The universal property of pullbacks (foundation)foundation.universal-property-pullbacks
The universal property of fiber productsfoundation.universal-property-fiber-products
Standard pullbacksfoundation.standard-pullbacks
Pullbacks (foundation-core)foundation-core.pullbacks
Pullbacks (foundation)foundation.pullbacks
Functoriality of pullbacksfoundation.functoriality-pullbacks
Cartesian morphisms of arrowsfoundation.cartesian-morphisms-arrows
Dependent products of pullbacksfoundation.dependent-products-pullbacks
Dependent sums of pullbacksfoundation.dependent-sums-pullbacks
Products of pullbacksfoundation.products-pullbacks
Coroducts of pullbacksfoundation.coproducts-pullbacks
Postcomposition of pullbacksfoundation.postcomposition-pullbacks
Pullbacks of subtypesfoundation.pullbacks-subtypes
The pullback-homorthogonal-factorization-systems.pullback-hom
Functoriality of the pullback-homorthogonal-factorization-systems.functoriality-pullback-hom
Pullbacks in precategoriescategory-theory.pullbacks-in-precategories