{-# OPTIONS --lossy-unification #-}
module Cubical.Categories.LocallySmall.Displayed.Instances.Functor.IntoFiberCategory where

open import Cubical.Foundations.Prelude

import Cubical.Data.Equality as Eq
open import Cubical.Data.Sigma.More


open import Cubical.Categories.LocallySmall.Category.Base
open import Cubical.Categories.LocallySmall.Category.Small
open import Cubical.Categories.LocallySmall.Instances.Functor.IntoFiberCategory
import Cubical.Categories.LocallySmall.Functor as LocallySmallF
open import Cubical.Categories.LocallySmall.Variables
open import Cubical.Categories.LocallySmall.Instances.ChangeOfObjects

open import Cubical.Categories.LocallySmall.Displayed.Category
import Cubical.Categories.LocallySmall.Displayed.Functor.Base as LocallySmallFᴰ
open import Cubical.Categories.LocallySmall.Displayed.Instances.ChangeOfObjects
open import Cubical.Categories.LocallySmall.Displayed.Instances.Reindex.Base
open import Cubical.Categories.LocallySmall.Displayed.Instances.BinProduct.Base
open import Cubical.Categories.LocallySmall.Displayed.NaturalTransformation.IntoFiberCategory.Base
open import Cubical.Categories.LocallySmall.Displayed.NaturalTransformation.IntoFiberCategory.Eq

open Category
open Categoryᴰ

open LocallySmallF.Functor
open LocallySmallFᴰ.Functorᴰ
open Liftω
open Σω

module _
  {C : SmallCategory ℓC ℓC'}
  {ℓCᴰ ℓCᴰ'}
  (Cᴰ : SmallCategoryᴰ C ℓCᴰ ℓCᴰ')
  {D : Category Dob DHom-ℓ}
  {Dobᴰ DHom-ℓᴰ}
  (Dᴰ : GloballySmallCategoryᴰ D Dobᴰ DHom-ℓᴰ)
  {Eob-ℓᴰ Eobᴰ EHom-ℓᴰ}
  (Eᴰ : SmallFibersCategoryᴰ D Eob-ℓᴰ Eobᴰ EHom-ℓᴰ)
  {Dᴰᴰ-ℓ Dobᴰᴰ DHom-ℓᴰᴰ}
  (Dᴰᴰ : SmallFibersᴰCategoryᴰ Dᴰ Eᴰ Dᴰᴰ-ℓ Dobᴰᴰ DHom-ℓᴰᴰ)
  where
  open NatTransᴰDefs Cᴰ Dᴰ Eᴰ Dᴰᴰ
  open FunctorEqᴰDefs Cᴰ Dᴰ Eᴰ Dᴰᴰ
  open NatTransᴰ
  private
    module C = SmallCategory C
    module Cᴰ = SmallCategoryᴰ Cᴰ
    module D = CategoryNotation D
    module Dᴰ = CategoryᴰNotation Dᴰ
    module Eᴰ = CategoryᴰNotation Eᴰ
    module Dᴰᴰ = CategoryᴰNotation Dᴰᴰ

    C⇒Eᴰ : Categoryᴰ D Functor _
    C⇒Eᴰ = FUNCTOR C Eᴰ

    Dᴰ×C⇒Eᴰ = Dᴰ ×ᴰ C⇒Eᴰ
    Dᴰ×Eᴰ = Dᴰ ×ᴰ Eᴰ
    module Dᴰ×C⇒Eᴰ = CategoryᴰNotation Dᴰ×C⇒Eᴰ
    module Dᴰ×Eᴰ = CategoryᴰNotation Dᴰ×Eᴰ

  FUNCTORᴰ :
    Categoryᴰ Dᴰ×C⇒Eᴰ.∫C (λ (d , dᴰ , F) → Functorᴰ F dᴰ) _
  FUNCTORᴰ .Hom[_][_,_] (f , fᴰ , α) =
    NatTransᴰ fᴰ α
  FUNCTORᴰ .idᴰ = idTransᴰ _
  FUNCTORᴰ ._⋆ᴰ_ = seqTransᴰ
  FUNCTORᴰ .⋆IdLᴰ αᴰ =
    makeNatTransᴰPath (Dᴰ×C⇒Eᴰ.⋆IdLᴰ _)
      (λ xᴰ → Dᴰᴰ.⋆IdLᴰ (αᴰ .N-obᴰ xᴰ))
  FUNCTORᴰ .⋆IdRᴰ  αᴰ =
    makeNatTransᴰPath (Dᴰ×C⇒Eᴰ.⋆IdRᴰ _)
      (λ xᴰ → Dᴰᴰ.⋆IdRᴰ (αᴰ .N-obᴰ xᴰ))
  FUNCTORᴰ .⋆Assocᴰ αᴰ βᴰ γᴰ =
    makeNatTransᴰPath (Dᴰ×C⇒Eᴰ.⋆Assocᴰ _ _ _)
      (λ xᴰ → Dᴰᴰ.⋆Assocᴰ (αᴰ .N-obᴰ xᴰ) (βᴰ .N-obᴰ xᴰ) (γᴰ .N-obᴰ xᴰ))
  FUNCTORᴰ .isSetHomᴰ = isSetNatTransᴰ _ _ _ _

  module _
    (D-⋆ : ∀ {x} → D.id D.⋆ D.id Eq.≡ D.id {x = x})
    (F-seq' : ∀ d dᴰ →
     {x y z : Liftω (Eobᴰ d)} (f : Hom[ fibEq Eᴰ D-⋆ d , x ] y)
      (g : Hom[ fibEq Eᴰ D-⋆ d , y ] z) →
      (Categoryᴰ.∫C (Dᴰ ×ᴰ Eᴰ) ⋆
       F-hom (fibᴰEqF D Dᴰ Eᴰ Dᴰᴰ d dᴰ D-⋆) f)
      (F-hom (fibᴰEqF D Dᴰ Eᴰ Dᴰᴰ d dᴰ D-⋆) g)
      Eq.≡
      F-hom (fibᴰEqF D Dᴰ Eᴰ Dᴰᴰ d dᴰ D-⋆)
      ((fibEq Eᴰ D-⋆ d ⋆ f) g)) where
    private

      C⇒EqEᴰ : Categoryᴰ D (FunctorEq D-⋆) _
      C⇒EqEᴰ = FUNCTOR-EQ C Eᴰ D-⋆

      Dᴰ×C⇒EqEᴰ = Dᴰ ×ᴰ C⇒EqEᴰ
      module Dᴰ×C⇒EqEᴰ = CategoryᴰNotation Dᴰ×C⇒EqEᴰ

    FUNCTOR-EQᴰ :
      Categoryᴰ Dᴰ×C⇒EqEᴰ.∫C (λ (d , dᴰ , F) → FunctorEqᴰ D-⋆ (F-seq' _ _) F dᴰ) _
    FUNCTOR-EQᴰ =
      reindexEq F Xᴰ Eq.refl λ _ _ → Eq.refl
      where
      changeObs :
        Σω[ d ∈ Dob ] Σω[ dᴰ ∈ Dobᴰ d ] FunctorEq D-⋆ d →
        Σω[ d ∈ Dob ] Σω[ dᴰ ∈ Dobᴰ d ] Functor d
      changeObs (d , dᴰ , F) = d , dᴰ , FunctorEq→Functor D-⋆ d F

      X : Category _ _
      X = ChangeOfObjects Dᴰ×C⇒Eᴰ.∫C changeObs

      Xᴰ : Categoryᴰ X
        (λ (d , dᴰ , F) →
          FunctorEqᴰ D-⋆ (F-seq' _ _)
            F dᴰ) _
      Xᴰ = ChangeOfObjectsᴰ.ChangeOfObjectsᴰ FUNCTORᴰ
        λ {(d , dᴰ , F)} Fᴰ → FunctorEqᴰ→Functorᴰ D-⋆
          (F-seq' _ _) Fᴰ

      F : LocallySmallF.Functor Dᴰ×C⇒EqEᴰ.∫C X
      F .F-ob = λ z → z
      F .F-hom = λ z → z
      F .F-id = refl
      F .F-seq = λ _ _ → refl