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

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

theory Symbols =
   Sigma   # Σ V1T,… . 2   prec -10000 ❙
   Product # 1×…           prec  -9990❙
   Tuple   # ⟨ 1,… ⟩				prec -10000 ❙
   Projl   # πl 1						prec -900 ❙
   Projr   # πr 1						prec -900 ❙
❚

theory Rules =
   rule rules?SigmaTerm ❙
   rule rules?TupleTerm ❙
   rule rules?Projection1Term ❙
   rule rules?Projection2Term ❙
   rule rules?SigmaType ❙
   rule rules?SigmaEquality ❙
   rule rules?TupleEquality ❙
   rule rules?Projection1Beta ❙
   rule rules?Projection2Beta ❙
   rule rules?SigmaSubtype ❙
❚
   
theory TypedSigma : ur:?TermsTypesKinds =
	include ?Symbols ❙
	include ?Rules ❙
❚
   
theory LFSigma =
	include ?TypedSigma ❙
	include ☞ur:?LF ❙
❚