{-

  The slice category over a displayed category. Used in the definition
  of a fibration.

-}

module Cubical.Categories.Displayed.Constructions.Slice where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma
open import Cubical.Data.Unit
import      Cubical.Data.Equality as Eq
open import Cubical.Categories.Category.Base
open import Cubical.Categories.Morphism
open import Cubical.Categories.NaturalTransformation
open import Cubical.Categories.Constructions.TotalCategory as TotalCat
open import Cubical.Categories.Displayed.Constructions.PropertyOver
open import Cubical.Categories.Displayed.Constructions.TotalCategory
  as TotalCatᴰ hiding (introF)
open import Cubical.Categories.Constructions.BinProduct as BP
open import Cubical.Categories.Constructions.BinProduct.More as BP
open import Cubical.Categories.Functor.Base
open import Cubical.Categories.Displayed.Base as Disp
open import Cubical.Categories.Displayed.Constructions.Weaken.Base as Wk
  hiding (introF)
open import Cubical.Categories.Displayed.Constructions.Reindex.Eq as Reindex
open import Cubical.Categories.Displayed.BinProduct
open import Cubical.Categories.Displayed.Constructions.BinProduct.More as BPᴰ
  hiding (introF)
open import Cubical.Categories.Displayed.Functor
open import Cubical.Categories.Displayed.Functor.More
open import Cubical.Categories.Displayed.Instances.Arrow
open import Cubical.Categories.Displayed.Instances.Terminal as Unitᴰ
  hiding (introF)
open import Cubical.Categories.Displayed.HLevels
open import Cubical.Categories.Displayed.Reasoning
open import Cubical.Categories.Displayed.Section.Base
private
  variable
    ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' : Level

open Category
open Categoryᴰ
open Functor

-- Do we actually need this?
-- module _ (C : Category ℓC ℓC') (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ') where
--   private module Slice = EqReindex Cᴰ {!!} {!!} {!!} -- Eq.refl (λ _ _ → Eq.refl)
--   -- See test below for the intuitive definition
--   _/C_ : Categoryᴰ C _ _
--   _/C_ = ∫Cᴰ (weaken C C) ({!!} ×ᴰ {!!}) -- (Cᴰ' ×ᴰ Arrow C)
--     where Cᴰ' = Slice.reindex

--   module _ {D : Category ℓD ℓD'}{Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'}
--     {F : Functor D C}
--     (Fᴰ₁ : Functor D C)
--     (Fᴰ₂ : Functorᴰ Fᴰ₁ Dᴰ Cᴰ)
--     (Fᴰ₃ : F ⇒ Fᴰ₁)
--     where
--     -- NOTE: this is not the most general introduction rule possible.
--     -- A more general version would allow Fᴰ₁ to depend on Dᴰ as well.
--     introF : Functorᴰ F Dᴰ _/C_
--     introF = TotalCatᴰ.introF _ _ (Wk.introF F Fᴰ₁)
--       (BPᴰ.introS _
--         (Slice.introS _ (reindS' (Eq.refl , Eq.refl) (TotalCat.elim Fᴰ₂)))
--         (reindS' (Eq.refl , Eq.refl)
--           (compSectionFunctor (arrIntroS {F1 = F} {F2 = Fᴰ₁} Fᴰ₃)
--             (TotalCat.Fst {Cᴰ = Dᴰ}))))

--   private
--     open Category
--     open Categoryᴰ
--     test : ∀ {c} → _/C_ .ob[_] c ≡ (Σ[ c' ∈ C .ob ] Cᴰ .ob[_] c' × C [ c , c' ])
--     test = refl

--   Δ/C : Functorᴰ Id Cᴰ _/C_
--   Δ/C = introF Id 𝟙ᴰ⟨ Cᴰ ⟩ (idTrans Id)

--   private
--     open Functorᴰ
--     _ : ∀ c (cᴰ : Cᴰ .ob[_] c) → Δ/C .F-obᴰ cᴰ ≡ (c , (cᴰ , C .id))
--     _ = λ c cᴰ → refl

-- -- module _ {C : Category ℓC ℓC'} {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'}
-- --   {D : Category ℓD ℓD'} {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'}
-- --   {F : Functor C D}
-- --   (Fᴰ₁ : Functor C D)
-- --   where
-- --   introF : Functorᴰ F Cᴰ (D /C Dᴰ)
-- --   introF = TotalCatᴰ.introF _ _ (Wk.introF F Fᴰ₁) {!Slice.introS!}

-- module _ (C : Category ℓC ℓC') where
--   -- Slices .ob[ c ] = Σ[ c' ∈ C .ob] C [ c' , c ]
--   Slices : Categoryᴰ C (ℓ-max ℓC ℓC') (ℓ-max ℓC' ℓC')
--   Slices = ∫Cᴰ (weaken C C) (Arrow C)

--   private
--     open Category
--     open Categoryᴰ
--     test : ∀ {c} → Slices .ob[_] c ≡ (Σ[ c' ∈ C .ob ] C [ c , c' ])
--     test = refl

--   Subobjects : Categoryᴰ C _ _
--   Subobjects = ∫Cᴰ (weaken C C) (Mono C)
--   private
--     open Category
--     open Categoryᴰ
--     test' : ∀ {c} → Subobjects .ob[_] c
--       ≡ (Σ[ c' ∈ C .ob ] Σ[ f ∈ C [ c , c' ] ] isMonic C f)
--     test' = refl