module Cat.Displayed.InternalSum {o ℓ o' ℓ'} {B : Precategory o ℓ} (E : Displayed B o' ℓ') where
Internal sums🔗
As has been noted before, fibrations are an excellent setting for studying logical and type-theoretic phenomena. Internal sums are an example of this; serving as the categorical analog of Sigma types.
To begin our definition, we first need a notion of a family internal to a fibration: this is handled by the fibration of displayed families. We say that a fibration has internal sums if the constant displayed family functor has a fibred left adjoint.
record Internal-sum : Type (o ⊔ ℓ ⊔ o' ⊔ ℓ') where no-eta-equality field ∐ : Vertical-fibred-functor (Disp-family E) E adjunction : ∐ ⊣↓ ConstDispFamVf E