open import Cat.Prelude

module Cat.Instances.Lift where


# Lifting categories across universesπ

Suppose you have a category $\mathcal{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 $\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