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' βŠ” β„“')
    ∐ : Vertical-fibred-functor (Disp-family E) E
    adjunction : ∐ βŠ£β†“ ConstDispFamVf E