module Cat.Instances.Lift where

Lifting categories across universesπŸ”—

Suppose you have a category with objects in and homs in but you really need it to have objects in some larger universe and homs in Fortunately you can uniformly lift the precategory 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) = G .Fβ‚€ x
  F .F₁ (lift f) = G .F₁ f
  F .F-id = G .F-id
  F .F-∘ (lift f) (lift g) = G .F-∘ 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 $ G .Fβ‚€ x
  F .F₁ f = lift $ G .F₁ f
  F .F-id = ap lift $ G .F-id
  F .F-∘ f g = ap lift $ G .F-∘ f g