Permutations of spans of families of types

Content created by Egbert Rijke.

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

module foundation.permutations-spans-families-of-types where
Imports 
open import foundation.dependent-pair-types
open import foundation.spans-families-of-types
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.function-types

Idea

Permutations of spans of families of types are a generalization of the opposite of a binary span. Consider a span (S , f) on a type family A : I → 𝒰 and an equivalence e : I ≃ I. Then the permutation is the span (S , f ∘ e) on the type family A ∘ e.

Definitions

Permutations of spans of families of types

module _
  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2}
  where

  permutation-span-type-family :
    (e : I ≃ I) → span-type-family l3 A →
    span-type-family l3 (A ∘ map-equiv e)
  pr1 (permutation-span-type-family e s) =
    spanning-type-span-type-family s
  pr2 (permutation-span-type-family e s) i =
    map-span-type-family s (map-equiv e i)

Recent changes