open import Cat.Prelude

module Cat.Instances.Lift where


# Lifting categories across universesπ

Suppose you have a category $\ca{C}$ with objects in $o$ and homs in $\ell$, but you really need it to have objects in some larger universe $o \sqcup o'$ and homs in $\ell \sqcup \ell'$. Fortunately you can uniformly lift the precategory $\ca{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