Cubical.Categories.Constructions.Slice.Properties

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

open import Cubical.Data.Sigma

open import Cubical.HITs.PropositionalTruncation using (∣_∣₁)

open import Cubical.Categories.Category
open import Cubical.Categories.Constructions.Slice.Base
import Cubical.Categories.Constructions.Elements as Elements
open import Cubical.Categories.Equivalence
open import Cubical.Categories.Functor
open import Cubical.Categories.Instances.Sets
open import Cubical.Categories.NaturalTransformation

open Category

module Cubical.Categories.Constructions.Slice.Properties
  {ℓC ℓ'C : Level}
  (C : Category ℓC ℓ'C)
  (c : C .ob)
  where

open Elements.Contravariant {C = C}

open _≃ᶜ_
open Functor
open WeakInverse

slice→el : Functor (SliceCat C c) (∫ᴾ (C [-, c ]))
slice→el .F-ob s = s .S-ob , s .S-arr
slice→el .F-hom f = f .S-hom , f .S-comm
slice→el .F-id = ΣPathP (refl , (isOfHLevelPath' 1 (C .isSetHom) _ _ _ _))
slice→el .F-seq _ _ = ΣPathP (refl , (isOfHLevelPath' 1 (C .isSetHom) _ _ _ _))

el→slice : Functor (∫ᴾ (C [-, c ])) (SliceCat C c)
el→slice .F-ob (_ , s) = sliceob s
el→slice .F-hom (f , comm) = slicehom f comm
el→slice .F-id = SliceHom-≡-intro C c refl (isOfHLevelPath' 1 (C .isSetHom) _ _ _ _)
el→slice .F-seq _ _ = SliceHom-≡-intro C c refl (isOfHLevelPath' 1 (C .isSetHom) _ _ _ _)

open NatTrans
open NatIso

sliceIsElementsOfRep : SliceCat C c ≃ᶜ (∫ᴾ (C [-, c ]))
sliceIsElementsOfRep .func = slice→el
sliceIsElementsOfRep .isEquiv  = ∣ w-inv ∣₁
  where
    w-inv : WeakInverse slice→el
    w-inv .invFunc = el→slice
    w-inv .η .trans .N-ob s = SliceCat C c .id
    w-inv .η .trans .N-hom f = (SliceCat C c .⋆IdR f)
                             ∙ sym (SliceCat C c .⋆IdL f)
    w-inv .η .nIso x = isiso (SliceCat C c .id)
                             (SliceCat C c .⋆IdR _)
                             (SliceCat C c .⋆IdR _)
    w-inv .ε .trans .N-ob s = (∫ᴾ (C [-, c ])) .id
    w-inv .ε .trans .N-hom f = ((∫ᴾ (C [-, c ])) .⋆IdR f)
                             ∙ sym ((∫ᴾ (C [-, c ])) .⋆IdL f)
    w-inv .ε .nIso x = isiso ((∫ᴾ (C [-, c ])) .id)
                             ((∫ᴾ (C [-, c ])) .⋆IdR _)
                             ((∫ᴾ (C [-, c ])) .⋆IdR _)