Permutations of spans of families of types

Content created by Egbert Rijke.

Created 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)