Total category

open import category-theory.category
open import category-theory.displayed-category

module category-theory.total-category
  {o h o′ h′} {𝒞 : Category o h}
  (𝒟 : DisplayedCategory 𝒞 o′ h′) where

open import foundations.universe
open import foundations.identity-type
open import foundations.sigma-type
open import foundations.sigma-type-identity
open import foundations.h-level-sigma

private module 𝒞 = Category 𝒞
open DisplayedCategory 𝒟

∫ : Category (o ⊔ o′) (h ⊔ h′)
∫ = record
  { 𝒞 = record
    { Ob = Σ 𝒞.Ob Ob
    ; Hom = λ {(A , X) (B , Y) → Σ[ f ∈ 𝒞.Hom A B ] Hom f X Y}
    ; id = λ {(A , X) → 𝒞.id A , id X}
    ; _∘_ = λ {(g , g′) (f , f′) → g 𝒞.∘ f , g′ ∘ f′}
    }
  ; is-category = record
    { identˡ = λ {(f , f′) → toΣId (𝒞.identˡ f , identˡ f′)}
    ; identʳ = λ {(f , f′) → toΣId (𝒞.identʳ f , identʳ f′)}
    ; ident² = λ {(A , X) → toΣId (𝒞.ident² A , ident² X)}
    ; assoc = toΣId (𝒞.assoc , assoc)
    ; sym-assoc = toΣId (𝒞.sym-assoc , sym-assoc)
    ; is-set-hom = isSetΣ 𝒞.is-set-hom λ _ → is-set-hom
    }
  }