Transposition of pointed span diagrams

Content created by Egbert Rijke.

Created on 2024-03-13.
Last modified 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 𝒮)

Recent changes