# Opposite pointed spans

Content created by Egbert Rijke.

Created on 2024-03-13.
Last modified on 2024-03-13.

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