module Cubical.Categories.Constructions.Lift where

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

open import Cubical.Categories.Category
open import Cubical.Categories.Functor

private
  variable
    ℓ ℓ' : Level

open Category

module _ (C : Category ℓ ℓ') (ℓ'' : Level) where
  LiftHoms : Category ℓ (ℓ-max ℓ' ℓ'')
  LiftHoms .ob = C .ob
  LiftHoms .Hom[_,_] A B = Lift {j = ℓ''} (C [ A , B ])
  LiftHoms .id = lift (C .id)
  LiftHoms ._⋆_ f g = lift (f .lower ⋆⟨ C ⟩ g .lower)
  LiftHoms .⋆IdL f = cong lift (C .⋆IdL (f .lower))
  LiftHoms .⋆IdR f = cong lift (C .⋆IdR (f .lower))
  LiftHoms .⋆Assoc f g h = cong lift (C .⋆Assoc (f .lower) (g .lower) (h .lower))
  LiftHoms .isSetHom = isOfHLevelLift  (C .isSetHom)

  liftHoms : Functor C LiftHoms
  liftHoms .Functor.F-ob = λ z → z
  liftHoms .Functor.F-hom = lift
  liftHoms .Functor.F-id = refl
  liftHoms .Functor.F-seq f g = refl

  lowerHoms : Functor LiftHoms C
  lowerHoms .Functor.F-ob = λ z → z
  lowerHoms .Functor.F-hom = lower
  lowerHoms .Functor.F-id = refl
  lowerHoms .Functor.F-seq f g = refl