Transposition of span diagrams

Content created by Egbert Rijke.

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

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

Idea

The trasposition of a span diagram

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

is the span diagram

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

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

Definitions

Transposition of span diagrams

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

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

Recent changes