# Transposition of pointed span diagrams

Content created by Egbert Rijke.

Created on 2024-03-13.

module structured-types.transposition-pointed-span-diagrams where

Imports
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import structured-types.opposite-pointed-spans
open import structured-types.pointed-span-diagrams


## Idea

The trasposition of a pointed span diagram

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


is the pointed span diagram

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


In other words, the transposition of a pointed span diagram (A , B , s) is the pointed span diagram (B , A , opposite-pointed-span s) where opposite-pointed-span s is the opposite of the pointed span s from A to B.

## Definitions

### Transposition of pointed span diagrams

module _
{l1 l2 l3 : Level} (𝒮 : pointed-span-diagram l1 l2 l3)
where

transposition-pointed-span-diagram : pointed-span-diagram l2 l1 l3
pr1 transposition-pointed-span-diagram =
pointed-codomain-pointed-span-diagram 𝒮
pr1 (pr2 transposition-pointed-span-diagram) =
pointed-domain-pointed-span-diagram 𝒮
pr2 (pr2 transposition-pointed-span-diagram) =
opposite-pointed-span (pointed-span-pointed-span-diagram 𝒮)