Opposite cospans

Content created by Fredrik Bakke.

Created on 2026-02-12.
Last modified on 2026-02-12.

module foundation.opposite-cospans where
Imports 
open import foundation.cospans
open import foundation.dependent-pair-types
open import foundation.universe-levels

Idea

Consider a cospan (S , f , g) from A to B. The opposite cospan of (S , f , g) is the cospan (S , g , f) from B to A. In other words, the opposite of a cospan

       f         g
  A ------> S <------ B

is the cospan

       g         f
  B ------> S <------ A.

Definitions

The opposite of a cospan

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

Recent changes