module Cubical.Categories.LocallySmall.NaturalTransformation.IntoFiberCategory where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.HLevels.More
open import Cubical.Foundations.Isomorphism hiding (isIso)

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

open import Cubical.Reflection.RecordEquiv.More

open import Cubical.Categories.LocallySmall.Category.Base
open import Cubical.Categories.LocallySmall.Category.Small
open import Cubical.Categories.LocallySmall.Functor.IntoFiberCategory
open import Cubical.Categories.LocallySmall.Variables

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

open Category
open Categoryᴰ
open SmallCategory

module NatTransDefs
  (C : SmallCategory ℓC ℓC')
  {D : Category Dob DHom-ℓ}
  {Dobᴰ-ℓ Dobᴰ DHom-ℓᴰ}
  (Dᴰ : SmallFibersCategoryᴰ D Dobᴰ-ℓ Dobᴰ DHom-ℓᴰ)
  where
  private
    module C = SmallCategory C
    module D = CategoryNotation D
    module Dᴰ = CategoryᴰNotation Dᴰ
  open FunctorDefs C Dᴰ public
  module _
    {d d' : Dob} (g : D.Hom[ d , d' ])
    (F : Functor d)
    (G : Functor d')
    where
    private
      module F = FunctorNotation F
      module G = FunctorNotation G

    N-homTy :
      (N-ob : ∀ x → Dᴰ.Hom[ g ][ F.F-ob (liftω x) , G.F-ob (liftω x) ])
      → ∀ {x y} → (f  : C.Hom[ liftω x , liftω y ]) → Type _
    N-homTy N-ob {x} {y} f =
      (F.F-hom f Dᴰ.⋆ᴰ N-ob y) Dᴰ.∫≡ (N-ob x Dᴰ.⋆ᴰ G.F-hom f)

    record NatTrans : Type (ℓ-max (DHom-ℓ d d') (ℓ-max (DHom-ℓᴰ d d') $ ℓ-max ℓC' ℓC))
      where
      no-eta-equality
      constructor natTrans
      field
        N-ob : ∀ x → Dᴰ.Hom[ g ][ F.F-ob (liftω x) , G.F-ob (liftω x) ]
        N-hom : ∀ {x y} (f : C.Hom[ liftω x , liftω y ]) → N-homTy N-ob f

  open NatTrans

  idTrans : ∀ {d}(F : Functor d)
    → NatTrans D.id F F
  idTrans F .N-ob _ = Dᴰ.idᴰ
  idTrans F .N-hom f =
    Dᴰ.⋆IdRᴰ _
    ∙ (sym $ Dᴰ.⋆IdLᴰ _)

  seqTrans : ∀ {d d' d''}
    {g : D.Hom[ d , d' ]}{g' : D.Hom[ d' , d'' ]}
    {F G H}
    (α : NatTrans g F G)
    (β : NatTrans g' G H)
    → NatTrans (g D.⋆ g') F H
  seqTrans α β .N-ob x = α .N-ob x Dᴰ.⋆ᴰ β .N-ob x
  seqTrans {F = F} {H = H} α β .N-hom f =
      (sym $ Dᴰ.⋆Assocᴰ _ _ _)
      ∙ Dᴰ.⟨ N-hom α f ⟩⋆⟨⟩
      ∙ Dᴰ.⋆Assoc _ _ _
      ∙ Dᴰ.⟨⟩⋆⟨ N-hom β f ⟩
      ∙ (sym $ Dᴰ.⋆Assocᴰ _ _ _)

  module _
    {d d'}
    (g : D.Hom[ d , d' ])
    (F : Functor d)
    (G : Functor d')
    where
    private
      module F = FunctorNotation F
      module G = FunctorNotation G
    NatTransIsoΣ :
      Iso (NatTrans g F G)
        (Σ[ N-ob ∈ (∀ x → Dᴰ.Hom[ g ][ F.F-ob (liftω x) , G.F-ob (liftω x) ])]
        (∀ {x y}
          (f  : C.Hom[ liftω x , liftω y ])
          → N-homTy g F G N-ob f))
    unquoteDef NatTransIsoΣ = defineRecordIsoΣ NatTransIsoΣ (quote (NatTrans))

    isSetNatTrans : isSet (NatTrans g F G)
    isSetNatTrans = isSetIso NatTransIsoΣ
      (isSetΣSndProp (isSetΠ (λ _ → Dᴰ.isSetHomᴰ))
        (λ _ → isPropImplicitΠ2 λ _ _ → isPropΠ λ _ →
          isSetΣ D.isSetHom (λ _ → Dᴰ.isSetHomᴰ) _ _))

  module _
    {d d'}
    {g g' : D.Hom[ d , d' ]}
    {F : Functor d}
    {G : Functor d'}
    where
    private
      module F = FunctorNotation F
      module G = FunctorNotation G

    makeNatTransPathP :
      {α : NatTrans g F G}
      {β : NatTrans g' F G}
      → (g≡g' : g ≡ g')
      → PathP
          (λ i → ∀ x →
            Dᴰ.Hom[ g≡g' i ][ F.F-ob (liftω x) ,
                              G.F-ob (liftω x) ])
          (α .N-ob)
          (β .N-ob)
      → PathP (λ i → NatTrans (g≡g' i) F G) α β
    makeNatTransPathP g≡g' p i .N-ob x = p i x
    makeNatTransPathP {α = α} {β = β} g≡g' p i .N-hom {x = x} {y = y} f =
      isSet→SquareP (λ _ _ → isSetΣ D.isSetHom (λ _ → Dᴰ.isSetHomᴰ))
        (α .N-hom f) (β .N-hom f)
        (λ j → _ , (F.F-hom f Dᴰ.⋆ᴰ p j y))
        (λ j → _ , (p j x Dᴰ.⋆ᴰ G.F-hom f))
        i

  module _
    {d d'} {g g' : D.Hom[ d , d' ]}
    {F : Functor d}
    {G : Functor d'}
    {α : NatTrans g F G}
    {β : NatTrans g' F G}
    (g≡g' : g ≡ g')
    (p : ∀ x → α .N-ob x Dᴰ.∫≡ β .N-ob x)
    where

    makeNatTransPath :
      Path (Σ[ h ∈ (D.Hom[ d , d' ]) ] NatTrans h F G) ((_ , α)) ((_ , β))
    makeNatTransPath =
      ΣPathP
        (g≡g' ,
        makeNatTransPathP g≡g' (funExt λ x → Dᴰ.rectify (Dᴰ.≡out (p x))))