feat(types): native type-system decoration layer (#26)

Add Term::Sigma + TypeInfo sidecar (8 dimensions: Universe, Multiplicity, EffectRow, refinement, Modality, TemporalOp, Semiring, relational_arity). Wire Idris2 QTT, F* effects/refinement, Dedukti Sigma, GNN type-info edges. Sigma rendering in all backends.

Author: hyperpolymath

src/rust/agent/explanations.rs

@@ -301,6 +301,18 @@ impl ExplanationGenerator {
                     self.format_term(body)
                 )
             },
+            Term::Sigma {
+                param,
+                param_type,
+                body,
+            } => {
+                format!(
+                    "∃{}:{}. {}",
+                    param,
+                    self.format_term(param_type),
+                    self.format_term(body)
+                )
+            },
             Term::App { func, args } => {
                 let args_str: Vec<_> = args.iter().map(|a| self.format_term(a)).collect();
                 format!("({} {})", self.format_term(func), args_str.join(" "))

src/rust/aspect.rs

@@ -417,6 +417,9 @@ pub struct TheoremFeatures {
     /// Pi type (dependent function) count
     pub pi_count: usize,
 
+    /// Sigma type (dependent pair) count
+    pub sigma_count: usize,
+
     /// Universe levels used
     pub universe_levels: HashSet<usize>,
 
@@ -650,6 +653,9 @@ impl RuleBasedTagger {
             },
             Term::Pi {
                 param_type, body, ..
+            }
+            | Term::Sigma {
+                param_type, body, ..
             } => {
                 self.extract_symbols_recursive(param_type, symbols);
                 self.extract_symbols_recursive(body, symbols);
@@ -746,6 +752,11 @@ impl AspectTagger for RuleBasedTagger {
             total_matches += features.pi_count;
         }
 
+        if features.sigma_count > 0 {
+            *aspect_counts.entry(Aspect::DependentTypes).or_insert(0) += features.sigma_count;
+            total_matches += features.sigma_count;
+        }
+
         if !features.universe_levels.is_empty() {
             *aspect_counts.entry(Aspect::Universes).or_insert(0) += 1;
             total_matches += 1;
@@ -807,6 +818,13 @@ impl RuleBasedTagger {
                 self.analyze_term(param_type, features, depth + 1);
                 self.analyze_term(body, features, depth + 1);
             },
+            Term::Sigma {
+                param_type, body, ..
+            } => {
+                features.sigma_count += 1;
+                self.analyze_term(param_type, features, depth + 1);
+                self.analyze_term(body, features, depth + 1);
+            },
             Term::Universe(level) | Term::Type(level) | Term::Sort(level) => {
                 features.universe_levels.insert(*level);
             },

src/rust/core.rs

@@ -33,6 +33,13 @@ pub enum Term {
         body: Box<Term>,
     },
 
+    /// Dependent pair / sum (Sigma type) Σ(x: A). B
+    Sigma {
+        param: String,
+        param_type: Box<Term>,
+        body: Box<Term>,
+    },
+
     /// Type universe at level
     Type(usize),
 
@@ -121,6 +128,13 @@ impl fmt::Display for Term {
             } => {
                 write!(f, "(Π {}: {}. {})", param, param_type, body)
             },
+            Term::Sigma {
+                param,
+                param_type,
+                body,
+            } => {
+                write!(f, "(Σ {}: {}. {})", param, param_type, body)
+            },
             Term::Type(level) => write!(f, "Type{}", level),
             Term::Sort(level) => write!(f, "Sort{}", level),
             Term::Universe(level) => write!(f, "Type{}", level),
@@ -189,6 +203,10 @@ pub struct Hypothesis {
 
     /// Optional body (for definitions)
     pub body: Option<Term>,
+
+    /// Optional native type-system decoration.
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub type_info: Option<crate::types::TypeInfo>,
 }
 
 /// Proof context with available premises
@@ -222,13 +240,17 @@ pub struct Definition {
     pub name: String,
     pub ty: Term,
     pub body: Term,
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub type_info: Option<crate::types::TypeInfo>,
 }
 
 /// A variable declaration
 #[derive(Debug, Clone, Serialize, Deserialize)]
 pub struct Variable {
     pub name: String,
     pub ty: Term,
+    #[serde(default, skip_serializing_if = "Option::is_none")]
+    pub type_info: Option<crate::types::TypeInfo>,
 }
 
 /// A proof tactic/command

src/rust/exchange/dedukti.rs

@@ -211,6 +211,18 @@ impl DeduktiExporter {
                     Self::term_to_dedukti(body)
                 )
             },
+            Term::Sigma {
+                param,
+                param_type,
+                body,
+            } => {
+                format!(
+                    "(dk_sigma {} ({} => {}))",
+                    Self::term_to_dedukti(param_type),
+                    param,
+                    Self::term_to_dedukti(body)
+                )
+            },
             Term::Type(level) => format!("Type {}", level),
             Term::Sort(level) => format!("Sort {}", level),
             Term::Universe(level) => format!("Type {}", level),
@@ -224,6 +236,32 @@ impl DeduktiExporter {
         if trimmed.starts_with('(') && trimmed.ends_with(')') {
             // Unwrap parentheses and recurse
             Self::dedukti_to_term(&trimmed[1..trimmed.len() - 1])
+        } else if trimmed.starts_with("dk_sigma ") {
+            // Sigma type: dk_sigma A (x => B)
+            let rest = trimmed.trim_start_matches("dk_sigma ").trim();
+            // Split into the type part and the binder part (x => B)
+            if let Some(paren_start) = rest.find('(') {
+                let type_part = rest[..paren_start].trim();
+                let binder_part = rest[paren_start..].trim();
+                let inner = if binder_part.starts_with('(') && binder_part.ends_with(')') {
+                    &binder_part[1..binder_part.len() - 1]
+                } else {
+                    binder_part
+                };
+                if let Some(arrow_pos) = inner.find("=>") {
+                    let param = inner[..arrow_pos].trim().to_string();
+                    let body_str = inner[arrow_pos + 2..].trim();
+                    Term::Sigma {
+                        param,
+                        param_type: Box::new(Self::dedukti_to_term(type_part)),
+                        body: Box::new(Self::dedukti_to_term(body_str)),
+                    }
+                } else {
+                    Term::Const(trimmed.to_string())
+                }
+            } else {
+                Term::Const(trimmed.to_string())
+            }
         } else if trimmed.contains("->") {
             // Pi type: A -> B
             let parts: Vec<&str> = trimmed.splitn(2, "->").collect();
@@ -416,6 +454,28 @@ mod tests {
         assert_eq!(dk, "x");
     }
 
+    #[test]
+    fn test_term_to_dedukti_sigma() {
+        let term = Term::Sigma {
+            param: "x".to_string(),
+            param_type: Box::new(Term::Const("Nat".to_string())),
+            body: Box::new(Term::Const("Prop".to_string())),
+        };
+        let dk = DeduktiExporter::term_to_dedukti(&term);
+        assert!(dk.contains("dk_sigma"), "Sigma should render as dk_sigma, got: {}", dk);
+        assert!(dk.contains("Nat"), "Sigma param type should appear, got: {}", dk);
+    }
+
+    #[test]
+    fn test_dedukti_to_term_sigma() {
+        let dk = "dk_sigma Nat (x => Prop)";
+        let term = DeduktiExporter::dedukti_to_term(dk);
+        match term {
+            Term::Sigma { ref param, .. } => assert_eq!(param, "x"),
+            _ => panic!("Expected Sigma term, got: {:?}", term),
+        }
+    }
+
     #[test]
     fn test_import_with_definition() {
         let module = DeduktiModule {

src/rust/gnn/embeddings.rs

@@ -184,9 +184,11 @@ impl TermFeatureExtractor {
         // Feature [29]: Contains quantifier (forall, exists, pi)
         if offset < FEATURE_DIM {
             features[offset] = if node.label.contains("pi_")
+                || node.label.contains("sigma_")
                 || node.label.contains("forall")
                 || node.label.contains("exists")
                 || node.label.contains("Pi")
+                || node.label.contains("Sigma")
             {
                 1.0
             } else {
@@ -304,6 +306,8 @@ fn infer_term_kind_from_label(label: &str) -> usize {
         3 // Lambda
     } else if label.starts_with("pi_") {
         4 // Pi
+    } else if label.starts_with("sigma_") {
+        13 // Sigma
     } else if label.starts_with("let_") {
         7 // Let
     } else if label.starts_with("fix_") {
@@ -344,6 +348,7 @@ fn term_kind_index(term: &Term) -> usize {
         Term::Hole(_) => 10,
         Term::Meta(_) => 11,
         Term::ProverSpecific { .. } => 12,
+        Term::Sigma { .. } => 13,
     }
 }
 
@@ -370,6 +375,9 @@ fn term_depth(term: &Term) -> usize {
         },
         Term::Pi {
             param_type, body, ..
+        }
+        | Term::Sigma {
+            param_type, body, ..
         } => 1 + term_depth(param_type).max(term_depth(body)),
         Term::Let {
             ty, value, body, ..
@@ -417,7 +425,7 @@ fn term_arity(term: &Term) -> usize {
                 1
             }
         },
-        Term::Pi { .. } => 2, // param_type + body
+        Term::Pi { .. } | Term::Sigma { .. } => 2, // param_type + body
         Term::Let { ty, .. } => {
             if ty.is_some() {
                 3