open import Cat.Prelude

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
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