namespace http://gl.mathhub.info/MMT/LFX/TypedHierarchy ❚
import rules scala://TypedHierarchy.LFX.mmt.kwarc.info❚
import lf scala://lf.mmt.kwarc.info ❚

fixmeta http://cds.omdoc.org/mmt?mmt ❚

theory Symbols =
   TypeLevel # 𝒰 1 prec -1000 ❙
   UnspecifiedTypeLevel # 𝒰 prec -999 ❙
❚

theory Rules =
	 rule rules?TypeLevelUniverse ❙
	 rule rules?TypeLevelSubRule ❙
	 rule rules?LevelType ❙
❚

theory TypedHierarchy =
   include ☞http://cds.omdoc.org/urtheories?ModExp❙
   include ☞ur:?Typed ❙
   include ☞ur:?Kinded ❙
   include ☞ur:?NatLiteralsOnly ❙
   include ?Symbols ❙
   include ?Rules ❙
   rule rules?LevelComputation ❙
❚

theory LFHierarchy =
   include ?TypedHierarchy ❙
   include ☞ur:?PLF ❙
   
   rule rules?PiHierarchy❙
   rule rules?LambdaHierarchy❙
   rule rules?Polymorphism❙
   rule rules?PolymorphismLambda ❙
❚