module Cubical.Categories.LocallySmall.Displayed.Constructions.Total where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels

open import Cubical.Data.Sigma
open import Cubical.Data.Sigma.More

open import Cubical.Categories.LocallySmall.Category.Base

open import Cubical.Categories.LocallySmall.Displayed.Category.Base
open import Cubical.Categories.LocallySmall.Displayed.Category.Small
open import Cubical.Categories.LocallySmall.Variables

open Category
open Categoryᴰ
open Σω
open Liftω

module _ {C : Category Cob CHom-ℓ}(Cᴰ : Categoryᴰ C Cobᴰ CHom-ℓᴰ) where
  private
    module C = CategoryNotation C
    module Cᴰ = Categoryᴰ Cᴰ
  module _ {Cobᴰᴰ CHom-ℓᴰᴰ}(Cᴰᴰ : Categoryᴰ Cᴰ.∫C Cobᴰᴰ CHom-ℓᴰᴰ) where
    private
      module Cᴰᴰ = Categoryᴰ Cᴰᴰ
    ∫Cᴰ : Categoryᴰ C (λ x → Σω[ xᴰ ∈ Cobᴰ x ] Cobᴰᴰ (x , xᴰ)) _
    ∫Cᴰ .Hom[_][_,_] f xᴰxᴰᴰ yᴰyᴰᴰ =
      Σ[ fᴰ ∈ Cᴰ.Hom[ f ][ xᴰxᴰᴰ .fst , yᴰyᴰᴰ .fst ] ]
        Cᴰᴰ.Hom[ f , fᴰ ][ xᴰxᴰᴰ .snd , yᴰyᴰᴰ .snd ]
    ∫Cᴰ .idᴰ = Cᴰ.idᴰ , Cᴰᴰ.idᴰ
    ∫Cᴰ ._⋆ᴰ_ ffᴰ ggᴰ = (ffᴰ .fst Cᴰ.⋆ᴰ ggᴰ .fst) , (ffᴰ .snd Cᴰᴰ.⋆ᴰ ggᴰ .snd)
    ∫Cᴰ .⋆IdLᴰ ffᴰ =
      ΣPathP ((C.⋆IdL _) , (
      ΣPathP ((Cᴰ.rectify $ Cᴰ.≡out $ Cᴰ.⋆IdLᴰ (ffᴰ .fst)) ,
      (Cᴰᴰ.rectify $ Cᴰᴰ.≡out $ Cᴰᴰ.⋆IdLᴰ (ffᴰ .snd)))))
    ∫Cᴰ .⋆IdRᴰ ffᴰ =
      ΣPathP ((C.⋆IdR _) , (
      ΣPathP ((Cᴰ.rectify $ Cᴰ.≡out $ Cᴰ.⋆IdRᴰ (ffᴰ .fst)) ,
      (Cᴰᴰ.rectify $ Cᴰᴰ.≡out $ Cᴰᴰ.⋆IdRᴰ (ffᴰ .snd)))))
    ∫Cᴰ .⋆Assocᴰ ffᴰ ggᴰ hhᴰ =
      ΣPathP (C.⋆Assoc _ _ _ ,
      (ΣPathP ((Cᴰ.rectify $ Cᴰ.≡out $ Cᴰ.⋆Assoc _ _ _) ,
      (Cᴰᴰ.rectify $ Cᴰᴰ.≡out $ Cᴰᴰ.⋆Assoc _ _ _))))
    ∫Cᴰ .isSetHomᴰ = isSetΣ Cᴰ.isSetHomᴰ (λ _ → Cᴰᴰ.isSetHomᴰ)

module _
  {C : Category Cob CHom-ℓ}
  {Cᴰ-ℓ}{Cobᴰ}{CHom-ℓᴰ}
  (Cᴰ : SmallFibersCategoryᴰ C Cᴰ-ℓ Cobᴰ CHom-ℓᴰ)
  where
  private
    module C = CategoryNotation C
    module Cᴰ = Categoryᴰ Cᴰ
  module _
    -- The levels of Cᴰᴰ only depend on the
    -- base objects in C
    {C-ℓᴰᴰ : Cob → Level}
    {Cobᴰᴰ}
    {CHom-ℓᴰᴰ : Cob → Cob → Level}
    (Cᴰᴰ :
      SmallFibersCategoryᴰ Cᴰ.∫C
        (λ x → C-ℓᴰᴰ (x .fst))
        Cobᴰᴰ (λ x y → CHom-ℓᴰᴰ (x .fst) (y .fst)))
    where
    private
      module Cᴰᴰ = Categoryᴰ Cᴰᴰ

    ∫CᴰSF :
      SmallFibersCategoryᴰ C _
        (λ (x : Cob) →
          Σ[ xᴰ ∈ Cobᴰ x ] Cobᴰᴰ (x , liftω xᴰ))
        _
    ∫CᴰSF .Hom[_][_,_] f xᴰxᴰᴰ yᴰyᴰᴰ =
      Σ[ fᴰ ∈
        Cᴰ.Hom[ f ][
          liftω (xᴰxᴰᴰ .lowerω .fst) ,
          liftω (yᴰyᴰᴰ .lowerω .fst) ] ]
        Cᴰᴰ.Hom[ f , fᴰ ][
          liftω (xᴰxᴰᴰ .lowerω .snd) ,
          liftω (yᴰyᴰᴰ .lowerω .snd) ]
    ∫CᴰSF .idᴰ = Cᴰ.idᴰ , Cᴰᴰ.idᴰ
    ∫CᴰSF ._⋆ᴰ_ fᴰ gᴰ =
      (fᴰ .fst Cᴰ.⋆ᴰ gᴰ .fst) ,
      (fᴰ .snd Cᴰᴰ.⋆ᴰ gᴰ .snd)
    ∫CᴰSF .⋆IdLᴰ ffᴰ =
      ΣPathP ((C.⋆IdL _) , (
      ΣPathP ((Cᴰ.rectify $ Cᴰ.≡out $ Cᴰ.⋆IdLᴰ (ffᴰ .fst)) ,
      (Cᴰᴰ.rectify $ Cᴰᴰ.≡out $ Cᴰᴰ.⋆IdLᴰ (ffᴰ .snd)))))
    ∫CᴰSF .⋆IdRᴰ ffᴰ =
      ΣPathP ((C.⋆IdR _) , (
      ΣPathP ((Cᴰ.rectify $ Cᴰ.≡out $ Cᴰ.⋆IdRᴰ (ffᴰ .fst)) ,
      (Cᴰᴰ.rectify $ Cᴰᴰ.≡out $ Cᴰᴰ.⋆IdRᴰ (ffᴰ .snd)))))
    ∫CᴰSF .⋆Assocᴰ ffᴰ ggᴰ hhᴰ =
      ΣPathP (C.⋆Assoc _ _ _ ,
      (ΣPathP ((Cᴰ.rectify $ Cᴰ.≡out $ Cᴰ.⋆Assoc _ _ _) ,
      (Cᴰᴰ.rectify $ Cᴰᴰ.≡out $ Cᴰᴰ.⋆Assoc _ _ _))))
    ∫CᴰSF .isSetHomᴰ = isSetΣ Cᴰ.isSetHomᴰ (λ _ → Cᴰᴰ.isSetHomᴰ)