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