{-# OPTIONS --lossy-unification #-}
module Cubical.Categories.LocallySmall.Displayed.Instances.BinProduct.Base where

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

import Cubical.Data.Equality as Eq
open import Cubical.Data.Sigma
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.Variables
open import Cubical.Categories.LocallySmall.Functor
open import Cubical.Categories.LocallySmall.Instances.Functor.IntoFiberCategory
open import Cubical.Categories.LocallySmall.NaturalTransformation.IntoFiberCategory
open import Cubical.Categories.LocallySmall.Instances.BinProduct.Base
open import Cubical.Categories.LocallySmall.Instances.BinProduct.Properties
open import Cubical.Categories.LocallySmall.Instances.Total.Properties as TotalCat

open import Cubical.Categories.LocallySmall.Displayed.Category.Base
open import Cubical.Categories.LocallySmall.Displayed.Category.Small
open import Cubical.Categories.LocallySmall.Displayed.Category.Notation
open import Cubical.Categories.LocallySmall.Displayed.Instances.Reindex.Base
open import Cubical.Categories.LocallySmall.Displayed.Instances.ChangeOfObjects
open import Cubical.Categories.LocallySmall.Displayed.Functor.Base
open import Cubical.Categories.LocallySmall.Displayed.Section.Base

open Category
open Categoryᴰ
open Σω

module _
  {C : Category Cob CHom-ℓ}(Cᴰ : Categoryᴰ C Cobᴰ CHom-ℓᴰ)
  {D : Category Dob DHom-ℓ}(Dᴰ : Categoryᴰ D Dobᴰ DHom-ℓᴰ)
  where
  private
    module C = CategoryNotation C
    module Cᴰ = Categoryᴰ Cᴰ
    module D = CategoryNotation D
    module Dᴰ = Categoryᴰ Dᴰ

  _×Cᴰ_ : Categoryᴰ (C ×C D)
            (λ (c , d) → Σω[ cᴰ ∈ Cobᴰ c ] Dobᴰ d)
            _
  _×Cᴰ_ .Hom[_][_,_] (f , g) (c , d) (c' , d') =
    Cᴰ.Hom[ f ][ c , c' ] × Dᴰ.Hom[ g ][ d , d' ]
  _×Cᴰ_ .idᴰ = Cᴰ.idᴰ , Dᴰ.idᴰ
  _×Cᴰ_ ._⋆ᴰ_ (fᴰ , gᴰ) (fᴰ' , gᴰ') = fᴰ Cᴰ.⋆ᴰ fᴰ' , gᴰ Dᴰ.⋆ᴰ gᴰ'
  _×Cᴰ_ .⋆IdLᴰ _ =
    ΣPathP (
      ΣPathP ((C.⋆IdL _) , (D.⋆IdL _)) ,
      ΣPathP ((Cᴰ.rectify $ Cᴰ.≡out $ Cᴰ.⋆IdLᴰ _) ,
              (Dᴰ.rectify $ Dᴰ.≡out $ Dᴰ.⋆IdLᴰ _)))
  _×Cᴰ_ .⋆IdRᴰ _ =
    ΣPathP (
      ΣPathP ((C.⋆IdR _) , (D.⋆IdR _)) ,
      ΣPathP ((Cᴰ.rectify $ Cᴰ.≡out $ Cᴰ.⋆IdRᴰ _) ,
              (Dᴰ.rectify $ Dᴰ.≡out $ Dᴰ.⋆IdRᴰ _)))
  _×Cᴰ_ .⋆Assocᴰ _ _ _ =
    ΣPathP (
      ΣPathP ((C.⋆Assoc _ _ _) , (D.⋆Assoc _ _ _)) ,
      ΣPathP ((Cᴰ.rectify $ Cᴰ.≡out $ Cᴰ.⋆Assocᴰ _ _ _) ,
              (Dᴰ.rectify $ Dᴰ.≡out $ Dᴰ.⋆Assocᴰ _ _ _)))
  _×Cᴰ_ .isSetHomᴰ = isSet× Cᴰ.isSetHomᴰ Dᴰ.isSetHomᴰ

  π₁ᴰ : Functorᴰ (π₁ C D) _×Cᴰ_ Cᴰ
  π₁ᴰ .Functorᴰ.F-obᴰ = λ z → z .fst
  π₁ᴰ .Functorᴰ.F-homᴰ = λ fᴰ → fᴰ .fst
  π₁ᴰ .Functorᴰ.F-idᴰ = refl
  π₁ᴰ .Functorᴰ.F-seqᴰ = λ _ _ → refl

  π₂ᴰ : Functorᴰ (π₂ C D) _×Cᴰ_ Dᴰ
  π₂ᴰ .Functorᴰ.F-obᴰ = λ z → z .snd
  π₂ᴰ .Functorᴰ.F-homᴰ = λ fᴰ → fᴰ .snd
  π₂ᴰ .Functorᴰ.F-idᴰ = refl
  π₂ᴰ .Functorᴰ.F-seqᴰ = λ _ _ → refl

module _
  {C : SmallCategory ℓC ℓC'}(Cᴰ : SmallCategoryᴰ C ℓCᴰ ℓCᴰ')
  {D : SmallCategory ℓD ℓC'}(Dᴰ : SmallCategoryᴰ D ℓDᴰ ℓDᴰ')
  where
  private
    module C = SmallCategory C
    module Cᴰ = SmallCategoryᴰ Cᴰ
    module D = SmallCategory D
    module Dᴰ = SmallCategoryᴰ Dᴰ

  open SmallCategoryᴰ
  _×Cᴰsmall_ : SmallCategoryᴰ (C ×Csmall D) _ _
  _×Cᴰsmall_ = smallcatᴰ _
    (ChangeOfObjectsᴰ.ChangeOfObjectsᴰ
      {X = Liftω (C.ob × D.ob)}
      {Y = λ (liftω (c , d)) → Liftω (Cᴰ.obᴰ c × Dᴰ.obᴰ d)}
      (Cᴰ.catᴰ ×Cᴰ Dᴰ.catᴰ)
      λ (liftω (cᴰ , dᴰ)) → liftω cᴰ , liftω dᴰ)

module _
  {C : Category Cob CHom-ℓ}
  (Cᴰ : Categoryᴰ C Cobᴰ CHom-ℓᴰ)
  (Dᴰ : Categoryᴰ C Dobᴰ DHom-ℓᴰ)
  where
  private
    module C = CategoryNotation C
    module Cᴰ = Categoryᴰ Cᴰ
    module Dᴰ = Categoryᴰ Dᴰ

    Δ : Functor C (C ×C C)
    Δ .Functor.F-ob = λ z → z , z
    Δ .Functor.F-hom = λ z → z , z
    Δ .Functor.F-id = refl
    Δ .Functor.F-seq = λ _ _ → refl

  _×ᴰ_ :
    Categoryᴰ C _ _
  _×ᴰ_ = reindexEq Δ (Cᴰ ×Cᴰ Dᴰ) Eq.refl (λ _ _ → Eq.refl)

module _
  {C : Category Cob CHom-ℓ}
  {D : Category Dob DHom-ℓ}
  {Cᴰ : Categoryᴰ C Cobᴰ CHom-ℓᴰ}
  {Dᴰ : Categoryᴰ D Dobᴰ DHom-ℓᴰ}
  {E : Category Eob EHom-ℓ}
  (F : Functor E C)
  (G : Functor E D)
  (Fᴰ : Section F Cᴰ) (Gᴰ : Section G Dᴰ)
  where
  private
    module Cᴰ = Categoryᴰ Cᴰ
    module Dᴰ = Categoryᴰ Dᴰ

  open Section
  introS-×Cᴰ : Section (F ,F G) (Cᴰ ×Cᴰ Dᴰ)
  introS-×Cᴰ .F-obᴰ = λ d → F-obᴰ Fᴰ d , F-obᴰ Gᴰ d
  introS-×Cᴰ .F-homᴰ = λ f → F-homᴰ Fᴰ f , F-homᴰ Gᴰ f
  introS-×Cᴰ .F-idᴰ =
    ΣPathP (ΣPathP ((Functor.F-id F) , (Functor.F-id G)) ,
      ΣPathP ((Cᴰ.rectify $ Cᴰ.≡out $ Fᴰ .F-idᴰ) ,
              (Dᴰ.rectify $ Dᴰ.≡out $ Gᴰ .F-idᴰ)))
  introS-×Cᴰ .F-seqᴰ fᴰ gᴰ =
    ΣPathP (ΣPathP ((Functor.F-seq F fᴰ gᴰ) , (Functor.F-seq G fᴰ gᴰ)) ,
      ΣPathP ((Cᴰ.rectify $ Cᴰ.≡out $ Fᴰ .F-seqᴰ fᴰ gᴰ) ,
              (Dᴰ.rectify $ Dᴰ.≡out $ Gᴰ .F-seqᴰ fᴰ gᴰ)))

module _
  {C : Category Cob CHom-ℓ}
  {D : Category Dob DHom-ℓ}
  {Cᴰ : Categoryᴰ C Cobᴰ CHom-ℓᴰ}
  {Dᴰ : Categoryᴰ D Dobᴰ DHom-ℓᴰ}
  {E : Category Eob EHom-ℓ}
  {Eᴰ : Categoryᴰ E Eobᴰ EHom-ℓᴰ}
  (F : Functor E C)
  (G : Functor E D)
  (Fᴰ : Functorᴰ F Eᴰ Cᴰ) (Gᴰ : Functorᴰ G Eᴰ Dᴰ)
  where
  private
    module Cᴰ = Categoryᴰ Cᴰ
    module Dᴰ = Categoryᴰ Dᴰ

  open Functorᴰ
  introF-×Cᴰ : Functorᴰ (F ,F G) Eᴰ (Cᴰ ×Cᴰ Dᴰ)
  introF-×Cᴰ .Functorᴰ.F-obᴰ = λ z → Functorᴰ.F-obᴰ Fᴰ z , Functorᴰ.F-obᴰ Gᴰ z
  introF-×Cᴰ .Functorᴰ.F-homᴰ = λ fᴰ → Functorᴰ.F-homᴰ Fᴰ fᴰ , Functorᴰ.F-homᴰ Gᴰ fᴰ
  introF-×Cᴰ .Functorᴰ.F-idᴰ =
    ΣPathP (ΣPathP ((Functor.F-id F) , (Functor.F-id G)) ,
      ΣPathP ((Cᴰ.rectify $ Cᴰ.≡out $ Fᴰ .F-idᴰ) ,
              (Dᴰ.rectify $ Dᴰ.≡out $ Gᴰ .F-idᴰ)))
  introF-×Cᴰ .Functorᴰ.F-seqᴰ fᴰ gᴰ =
    ΣPathP (ΣPathP ((Functor.F-seq F _ _) , (Functor.F-seq G _ _)) ,
      ΣPathP ((Cᴰ.rectify $ Cᴰ.≡out $ Fᴰ .F-seqᴰ fᴰ gᴰ) ,
              (Dᴰ.rectify $ Dᴰ.≡out $ Gᴰ .F-seqᴰ fᴰ gᴰ)))

module _
  {C : Category Cob CHom-ℓ}
  {Cᴰ : Categoryᴰ C Cobᴰ CHom-ℓᴰ}
  {Dᴰ : Categoryᴰ C Dobᴰ DHom-ℓᴰ}
  {E : Category Eob EHom-ℓ}
  (F : Functor E C)
  (Fᴰ : Section F Cᴰ) (Gᴰ : Section F Dᴰ)
  where
  private
    module Cᴰ = Categoryᴰ Cᴰ
    module Dᴰ = Categoryᴰ Dᴰ

  open Section
  introS : Section F (Cᴰ ×ᴰ Dᴰ)
  introS .F-obᴰ = λ d → F-obᴰ Fᴰ d , F-obᴰ Gᴰ d
  introS .F-homᴰ = λ f → F-homᴰ Fᴰ f , F-homᴰ Gᴰ f
  introS .F-idᴰ =
    ΣPathP (Functor.F-id F ,
      ΣPathP ((Cᴰ.rectify $ Cᴰ.≡out $ Fᴰ .F-idᴰ) ,
              (Dᴰ.rectify $ Dᴰ.≡out $ Gᴰ .F-idᴰ)))
  introS .F-seqᴰ fᴰ gᴰ =
    ΣPathP (Functor.F-seq F _ _ ,
      ΣPathP ((Cᴰ.rectify $ Cᴰ.≡out $ Fᴰ .F-seqᴰ fᴰ gᴰ) ,
              (Dᴰ.rectify $ Dᴰ.≡out $ Gᴰ .F-seqᴰ fᴰ gᴰ)))

module _
  {C : Category Cob CHom-ℓ}
  {Cᴰ : Categoryᴰ C Cobᴰ CHom-ℓᴰ}
  {Dᴰ : Categoryᴰ C Dobᴰ DHom-ℓᴰ}
  where
  private
    module C = CategoryNotation C
    module Cᴰ = CategoryᴰNotation Cᴰ
    module Dᴰ = Categoryᴰ Dᴰ
    module Cᴰ×Dᴰ = Categoryᴰ (Cᴰ ×ᴰ Dᴰ)
  module _
    {E : Category Eob EHom-ℓ}
    {Eᴰ : Categoryᴰ E Eobᴰ EHom-ℓᴰ}
    {F : Functor E C}
    (Fᴰ : Functorᴰ F Eᴰ Cᴰ)
    (Gᴰ : Functorᴰ F Eᴰ Dᴰ)
    where
    open Functorᴰ
    private
      module Eᴰ = CategoryᴰNotation Eᴰ
    introF : Functorᴰ F Eᴰ (Cᴰ ×ᴰ Dᴰ)
    introF =
      recᴰ Eᴰ
        (introS _
          (TotalCat.elim Eᴰ Fᴰ)
          (TotalCat.elim Eᴰ Gᴰ))

  module _
    {Eᴰ : Categoryᴰ C Eobᴰ EHom-ℓᴰ}
    (Fᴰ : Functorⱽ Eᴰ Cᴰ)
    (Gᴰ : Functorⱽ Eᴰ Dᴰ)
    where
    open Functorᴰ
    private
      module Eᴰ = CategoryᴰNotation Eᴰ
    -- Don't actually need this definition if
    -- Functor has eta equality
    -- you can just use introF
    introFⱽ : Functorⱽ Eᴰ (Cᴰ ×ᴰ Dᴰ)
    introFⱽ =
      recᴰ Eᴰ
        (introS _
          (TotalCat.elim Eᴰ Fᴰ)
          (TotalCat.elim Eᴰ Gᴰ))

module _
  {C : SmallCategory ℓC ℓC'}
  (Cᴰ : SmallCategoryᴰ C ℓCᴰ ℓCᴰ')
  (Dᴰ : SmallCategoryᴰ C ℓDᴰ ℓDᴰ')
  where
  open SmallCategory
  open SmallCategoryᴰ
  private
    module C = SmallCategory C
    module Cᴰ = SmallCategoryᴰ Cᴰ
    module Dᴰ = SmallCategoryᴰ Dᴰ

    Δ : Functor C.cat ((C ×Csmall C) .cat)
    Δ .Functor.F-ob = λ z → liftω (z .Liftω.lowerω , z .Liftω.lowerω)
    Δ .Functor.F-hom = λ z → z , z
    Δ .Functor.F-id = refl
    Δ .Functor.F-seq = λ _ _ → refl

  -- The fiberwise product of displayed categories arises as the
  -- pullback --- that is, the reindexing --- of the displayed
  -- product of categories
  _×ᴰsmall_ : SmallCategoryᴰ C _ _
  _×ᴰsmall_ = smallcatᴰ _ (reindexEq Δ ((Cᴰ ×Cᴰsmall Dᴰ) .catᴰ) Eq.refl λ _ _ → Eq.refl)

  _×ᴰsmall'_ : SmallCategoryᴰ C _ _
  _×ᴰsmall'_ = smallcatᴰ _ (reindex' Δ ((Cᴰ ×Cᴰsmall Dᴰ) .catᴰ))

module _
  {C : Category Cob CHom-ℓ}{Cobᴰ-ℓ Cobᴰ CHom-ℓᴰ}
  (Cᴰ : SmallFibersCategoryᴰ C Cobᴰ-ℓ Cobᴰ CHom-ℓᴰ)
  {D : Category Dob DHom-ℓ} {Dobᴰ-ℓ Dobᴰ DHom-ℓᴰ}
  (Dᴰ : SmallFibersCategoryᴰ D Dobᴰ-ℓ Dobᴰ DHom-ℓᴰ)
  where
  private
    module C = CategoryNotation C
    module Cᴰ = Categoryᴰ Cᴰ
    module D = CategoryNotation D
    module Dᴰ = Categoryᴰ Dᴰ

  _×CᴰSF_ : SmallFibersCategoryᴰ (C ×C D) _
            (λ (c , d) → Cobᴰ c × Dobᴰ d)
            _
  _×CᴰSF_ .Hom[_][_,_] (f , g) (liftω (c , d)) (liftω (c' , d')) =
    Cᴰ.Hom[ f ][ liftω c , liftω c' ] × Dᴰ.Hom[ g ][ liftω d , liftω d' ]
  _×CᴰSF_ .idᴰ = Cᴰ.idᴰ , Dᴰ.idᴰ
  _×CᴰSF_ ._⋆ᴰ_ (fᴰ , gᴰ) (fᴰ' , gᴰ') = fᴰ Cᴰ.⋆ᴰ fᴰ' , gᴰ Dᴰ.⋆ᴰ gᴰ'
  _×CᴰSF_ .⋆IdLᴰ _ =
    ΣPathP (
      ΣPathP ((C.⋆IdL _) , (D.⋆IdL _)) ,
      ΣPathP ((Cᴰ.rectify $ Cᴰ.≡out $ Cᴰ.⋆IdLᴰ _) ,
              (Dᴰ.rectify $ Dᴰ.≡out $ Dᴰ.⋆IdLᴰ _)))
  _×CᴰSF_ .⋆IdRᴰ _ =
    ΣPathP (
      ΣPathP ((C.⋆IdR _) , (D.⋆IdR _)) ,
      ΣPathP ((Cᴰ.rectify $ Cᴰ.≡out $ Cᴰ.⋆IdRᴰ _) ,
              (Dᴰ.rectify $ Dᴰ.≡out $ Dᴰ.⋆IdRᴰ _)))
  _×CᴰSF_ .⋆Assocᴰ _ _ _ =
    ΣPathP (
      ΣPathP ((C.⋆Assoc _ _ _) , (D.⋆Assoc _ _ _)) ,
      ΣPathP ((Cᴰ.rectify $ Cᴰ.≡out $ Cᴰ.⋆Assocᴰ _ _ _) ,
              (Dᴰ.rectify $ Dᴰ.≡out $ Dᴰ.⋆Assocᴰ _ _ _)))
  _×CᴰSF_ .isSetHomᴰ = isSet× Cᴰ.isSetHomᴰ Dᴰ.isSetHomᴰ

module _
  {C : Category Cob CHom-ℓ}{Cobᴰ-ℓ Cobᴰ CHom-ℓᴰ}
  (Cᴰ : SmallFibersCategoryᴰ C Cobᴰ-ℓ Cobᴰ CHom-ℓᴰ)
  {D : Category Dob DHom-ℓ} {Dobᴰ-ℓ Dobᴰ DHom-ℓᴰ}
  (Dᴰ : SmallFibersCategoryᴰ D Dobᴰ-ℓ Dobᴰ DHom-ℓᴰ)
  where
  private
    module C = CategoryNotation C
    module Cᴰ = CategoryᴰNotation Cᴰ
    module D = CategoryNotation D
    module C×D = CategoryNotation (C ×C D)
    module Dᴰ = CategoryᴰNotation Dᴰ
    module Cᴰ×Dᴰ = CategoryᴰNotation (Cᴰ ×CᴰSF Dᴰ)

  open Functor
  ×CᴰFiber→ProductOfFibers : ∀ {c} {d} →
    Functor Cᴰ×Dᴰ.v[ c , d ] (Cᴰ.v[ c ] ×C Dᴰ.v[ d ])
  ×CᴰFiber→ProductOfFibers .F-ob = λ z → liftω (z .Liftω.lowerω .fst) , liftω (z .Liftω.lowerω .snd)
  ×CᴰFiber→ProductOfFibers .F-hom = λ z → z
  ×CᴰFiber→ProductOfFibers .F-id = refl
  ×CᴰFiber→ProductOfFibers .F-seq _ _ = refl

  ProductOfFibers→×CᴰSFFiber :
    ∀ {c} {d} → Functor (Cᴰ.v[ c ] ×C Dᴰ.v[ d ]) Cᴰ×Dᴰ.v[ c , d ]
  ProductOfFibers→×CᴰSFFiber .F-ob = λ z → liftω (z .fst .Liftω.lowerω , z .snd .Liftω.lowerω)
  ProductOfFibers→×CᴰSFFiber .F-hom = λ z → z
  ProductOfFibers→×CᴰSFFiber .F-id = refl
  ProductOfFibers→×CᴰSFFiber .F-seq _ _ = refl

module _
  {D : Category Dob DHom-ℓ}
  {E : Category Eob EHom-ℓ}
  {Dobᴰ-ℓ Dobᴰ DHom-ℓᴰ}
  {Eobᴰ-ℓ Eobᴰ EHom-ℓᴰ}
  (C : SmallCategory ℓC ℓC')
  (Dᴰ : SmallFibersCategoryᴰ D Dobᴰ-ℓ Dobᴰ DHom-ℓᴰ)
  (Eᴰ : SmallFibersCategoryᴰ E Eobᴰ-ℓ Eobᴰ EHom-ℓᴰ)
  where
  private
    module C =  SmallCategory C
    module D =  CategoryNotation D
    module Dᴰ = CategoryᴰNotation Dᴰ
    module E =  CategoryNotation E
    module Eᴰ = CategoryᴰNotation Eᴰ
    module D×E =  CategoryNotation (D ×C E)
    module Dᴰ×ᴰEᴰ =  CategoryᴰNotation (Dᴰ ×CᴰSF Eᴰ)
    module FuncDᴰ = NatTransDefs C Dᴰ
    module NatTransDᴰ = FuncDᴰ.NatTrans
    module FuncEᴰ = NatTransDefs C Eᴰ
    module NatTransEᴰ = FuncEᴰ.NatTrans
    module FuncDᴰ×Eᴰ = NatTransDefs C (Dᴰ ×CᴰSF Eᴰ)
    module NatTransDᴰ×Eᴰ = FuncDᴰ×Eᴰ.NatTrans

  open Functorᴰ

  ,Fⱽ :
    Functorⱽ
      (FUNCTOR C Dᴰ ×Cᴰ FUNCTOR C Eᴰ)
      (FUNCTOR C (Dᴰ ×CᴰSF Eᴰ))
  ,Fⱽ .F-obᴰ (F , G) =
    ProductOfFibers→×CᴰSFFiber Dᴰ Eᴰ ∘F (F ,F G)
  ,Fⱽ .F-homᴰ fᴰ .NatTransDᴰ×Eᴰ.N-ob x = fᴰ .fst .NatTransDᴰ.N-ob x , fᴰ .snd .NatTransEᴰ.N-ob x
  ,Fⱽ .F-homᴰ {xᴰ = xᴰ}{yᴰ = yᴰ} (α , β) .NatTransDᴰ×Eᴰ.N-hom g =
       (ΣPathP (D×E.⋆IdL _ ∙ (sym $ D×E.⋆IdR _) ,
               ΣPathP (
                 (Dᴰ.rectify (Dᴰ.≡out $ NatTransDᴰ.N-hom α g)) ,
                 (Eᴰ.rectify (Eᴰ.≡out $ NatTransEᴰ.N-hom β g)))))
  ,Fⱽ .F-idᴰ =
    FuncDᴰ×Eᴰ.makeNatTransPath refl (λ _ → refl)
  ,Fⱽ .F-seqᴰ _ _ =
    FuncDᴰ×Eᴰ.makeNatTransPath refl (λ _ → refl)