Transposition of cospan diagrams

Content created by Fredrik Bakke.

Created on 2026-02-12.
Last modified on 2026-02-12.

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

Idea

The transposition of a cospan diagram

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

is the cospan diagram

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

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

Definitions

Transposition of cospan diagrams

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

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

Recent changes