module Cat.Instances.Graphs.Lift where
Lifting graphs🔗
This page defines a technical construction: we can lift a graph to have both its nodes and edges live in a higher universe level. This is analogous to lifting categories across universes.
Liftᴳ : ∀ o' ℓ' → Graph o ℓ → Graph (o ⊔ o') (ℓ ⊔ ℓ') Liftᴳ o' ℓ' G .Node = Lift o' (G .Node) Liftᴳ o' ℓ' G .Edge (lift x) (lift y) = Lift ℓ' (G .Edge x y) Liftᴳ o' ℓ' G .Node-set = hlevel 2 Liftᴳ o' ℓ' G .Edge-set = hlevel 2 lowerᴳ : Graph-hom (Liftᴳ o' ℓ' G) G lowerᴳ .node = lower lowerᴳ .edge = lower liftᴳ : Graph-hom G (Liftᴳ o' ℓ' G) liftᴳ .node = lift liftᴳ .edge = lift