open import Cat.Prelude

module Cat.Instances.Lift where

Lifting categories across universesπŸ”—

Suppose you have a category C\mathcal{C} with objects in oo and homs in β„“\ell, but you really need it to have objects in some larger universe oβŠ”oβ€²o \sqcup o' and homs in β„“βŠ”β„“β€²\ell \sqcup \ell'. Fortunately you can uniformly lift the precategory C\mathcal{C} to this bigger universe.

Lift-cat : βˆ€ {o β„“} oβ€² β„“β€² β†’ Precategory o β„“ β†’ Precategory (o βŠ” oβ€²) (β„“ βŠ” β„“β€²)
Lift-cat oβ€² β„“β€² C = liftc where
  open Precategory C
  open HLevel-instance
  liftc : Precategory _ _
  liftc .Precategory.Ob = Lift oβ€² Ob
  liftc .Precategory.Hom (lift x) (lift y) = Lift β„“β€² (Hom x y)
  liftc .Precategory.Hom-set x y = hlevel 2
  liftc .Precategory.id = lift id
  liftc .Precategory._∘_ (lift f) (lift g) = lift (f ∘ g)
  liftc .Precategory.idr (lift f) = ap lift (idr f)
  liftc .Precategory.idl (lift f) = ap lift (idl f)
  liftc .Precategory.assoc (lift f) (lift g) (lift h) = ap lift (assoc f g h)

Lift-functor-l
  : βˆ€ {so sβ„“} bo bβ„“ {o β„“} {C : Precategory so sβ„“} {D : Precategory o β„“}
  β†’ Functor C D
  β†’ Functor (Lift-cat bo bβ„“ C) D
Lift-functor-l bo bβ„“ G = F where
  open Functor
  F : Functor _ _
  F .Fβ‚€ (lift x) = Fβ‚€ G x
  F .F₁ (lift f) = F₁ G f
  F .F-id = F-id G
  F .F-∘ (lift f) (lift g) = F-∘ G f g

Lift-functor-r
  : βˆ€ {so sβ„“} bo bβ„“ {o β„“} {C : Precategory so sβ„“} {D : Precategory o β„“}
  β†’ Functor C D
  β†’ Functor C (Lift-cat bo bβ„“ D)
Lift-functor-r bo bβ„“ G = F where
  open Functor
  F : Functor _ _
  F .Fβ‚€ x = lift $ Fβ‚€ G x
  F .F₁ f = lift $ F₁ G f
  F .F-id = ap lift $ F-id G
  F .F-∘ f g = ap lift $ F-∘ G f g