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 E\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