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
$\mathcal{E}$
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