This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Opposite pointed spans

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

open import structured-types.pointed-spans
open import structured-types.pointed-types

Idea

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

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

is the pointed span

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

Definitions

The opposite of a pointed span

module _
  {l1 l2 l3 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2}
  where

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

See also