Opposite spans

Content created by Egbert Rijke.

Created on 2024-01-28.
Last modified on 2024-01-28.

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

Idea

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

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

is the span

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

Recall that binary type duality shows that spans are equivalent to binary relations from A to B. The opposite of a span corresponds to the opposite of a binary relation.

Definitions

The opposite of a span

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
  where

  opposite-span : span l3 A B → span l3 B A
  pr1 (opposite-span s) = spanning-type-span s
  pr1 (pr2 (opposite-span s)) = right-map-span s
  pr2 (pr2 (opposite-span s)) = left-map-span s

See also

Recent changes