module Cat.Displayed.InternalSum {o β oβ² ββ²} {B : Precategory o β} (E : Displayed B oβ² ββ²) where open Precategory B open Displayed E open import Cat.Displayed.Instances.Slice B open import Cat.Displayed.Total

# 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