# Operations on spans of families of types

Content created by Egbert Rijke.

Created on 2024-01-28.

module foundation.operations-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.function-types


## Idea

This file contains a collection of operations that produce new spans of families of types from given spans of families of types.

## Definitions

### Concatenation of spans and families of maps

Consider a span 𝒮 := (S , s) on a family of types A : I → 𝒰 and consider a family of maps f : (i : I) → A i → B i. Then we can concatenate the span 𝒮 with the family of maps f to obtain the span (S , λ i → f i ∘ s i) on B.

module _
{l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
(𝒮 : span-type-family l4 A)
(f : (i : I) → A i → B i)
where

spanning-type-concat-span-hom-family-of-types : UU l4
spanning-type-concat-span-hom-family-of-types =
spanning-type-span-type-family 𝒮

map-concat-span-hom-family-of-types :
(i : I) → spanning-type-concat-span-hom-family-of-types → B i
map-concat-span-hom-family-of-types i =
f i ∘ map-span-type-family 𝒮 i

concat-span-hom-family-of-types :
span-type-family l4 B
pr1 concat-span-hom-family-of-types =
spanning-type-concat-span-hom-family-of-types
pr2 concat-span-hom-family-of-types =
map-concat-span-hom-family-of-types