namespace http://gl.mathhub.info/MMT/LFX/Subtyping ❚

import rules scala://Subtyping.LFX.mmt.kwarc.info❚

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

theory PiRule =
  rule rules?PiRule ❙
❚
  
theory LFWithVariance =
	include ☞ur:?LF ❙
	include ?PiRule ❙
❚

theory SubSymbol =
	subtypeOf # %n 1 prec -9996 ❙
❚
  
theory SubRules =
	rule rules?SubUniverseRule ❙
	rule rules?SubUniverseType ❙
  rule rules?SubtypeOfRule ❙
  rule rules?SubtypeOfTypeRule ❙
❚
  
theory LFPowerTypes =
	include ?SubSymbol ❙
	include ?SubRules ❙
	include ?LFWithVariance ❙
❚
	

theory JudgmentSymbol =
	subtypeJudge # 1 <* 2 prec -9995 ❙
❚
  
theory JudgmentRules =
  rule rules?SubJudgUniverseType ❙
  // rule rules?SubJudgRule ❙
❚
  
theory LFSubJudgment =
	include ?JudgmentSymbol ❙
	include ?JudgmentRules ❙
	include ?LFWithVariance ❙
❚

theory PredSubSymbols =
	predsubtp # ⟨ V1T | 2 ⟩ prec -10001 ❙
  PredOf # PredOf 1 ❙
❚
  
theory PredSubRules =
  rule rules?Predsubtype ❙
  rule rules?Predsubrule ❙
  rule rules?PredsubTyping ❙
  rule rules?PredOfTerm ❙
❚
  
theory LFPredSub =
	include ?PredSubSymbols ❙
	include ?PredSubRules ❙
	include ?LFWithVariance ❙
❚
  
theory AllSubtypes =
	// include ?SubSymbol ❙
	// include ?SubRules ❙
	include ?JudgmentSymbol ❙
	include ?JudgmentRules ❙
	include ?PredSubSymbols ❙
	include ?PredSubRules ❙
❚
  
theory LFSubtyped =
	include ?AllSubtypes ❙
	include ?LFWithVariance ❙
❚