From 114747bb3dd1c0443a0e659133fadfb891efa052 Mon Sep 17 00:00:00 2001
From: imiel <imiel@engineer.city>
Date: Sun, 19 Apr 2026 18:06:54 +0000
Subject: [PATCH] Add definitional transport and congruence combinators derived
 from Id so equality programming isnt all raw idElim

---
 BidirTT/Examples.lean | 38 ++++++++++++++++++++++++++++++++++++++
 Main.lean             |  4 ++++
 Tests.lean            |  8 ++++++++
 3 files changed, 50 insertions(+)

diff --git a/BidirTT/Examples.lean b/BidirTT/Examples.lean
index 78c09a1..5b1c3be 100644
--- a/BidirTT/Examples.lean
+++ b/BidirTT/Examples.lean
@@ -74,6 +74,44 @@ def idElimNat : Raw :=
     (.idElim "y" "p" .nat .zero .zero reflZero)
     .nat
 
+def transportNatTy : Raw :=
+  .pi "x" .nat
+    (.pi "y" .nat
+      (.pi "p" (.id .nat (.var "x") (.var "y"))
+        (.pi "z" .nat .nat)))
+
+def transportNatTm : Raw :=
+  .lam "x" (.lam "y" (.lam "p" (.lam "z"
+    (.idElim "y'" "p'" .nat (.var "z") (.var "y") (.var "p")))))
+
+def transportNat : Raw := .ann transportNatTm transportNatTy
+
+def transportNatRefl : Raw :=
+  .ann
+    (.app (.app (.app (.app transportNat .zero) .zero) reflZero) natTwo)
+    .nat
+
+def congSuccTy : Raw :=
+  .pi "x" .nat
+    (.pi "y" .nat
+      (.pi "p" (.id .nat (.var "x") (.var "y"))
+        (.id .nat (.succ (.var "x")) (.succ (.var "y")))))
+
+def congSuccTm : Raw :=
+  .lam "x" (.lam "y" (.lam "p"
+    (.idElim "y'" "p'"
+      (.id .nat (.succ (.var "x")) (.succ (.var "y'")))
+      .refl
+      (.var "y")
+      (.var "p"))))
+
+def congSucc : Raw := .ann congSuccTm congSuccTy
+
+def congSuccRefl : Raw :=
+  .ann
+    (.app (.app (.app congSucc .zero) .zero) reflZero)
+    (.id .nat (.succ .zero) (.succ .zero))
+
 def omegaTy : Raw :=
   .pi "A" (.univ 0) (.var "A")
 
diff --git a/Main.lean b/Main.lean
index e51a79b..a688fd9 100644
--- a/Main.lean
+++ b/Main.lean
@@ -28,6 +28,10 @@ def main : IO Unit := do
   runOne "empty absurd"  Examples.absurdNat
   runOne "refl zero"     Examples.reflZero
   runOne "id elim"       Examples.idElimNat
+  runOne "transport nat" Examples.transportNat
+  runOne "transport refl" Examples.transportNatRefl
+  runOne "cong succ"     Examples.congSucc
+  runOne "cong succ refl" Examples.congSuccRefl
   runOne "let universe"  Examples.letUniverse
   runOne "omega (bad)"   Examples.omegaAnn
   runOne "unknown var"   Examples.unknownVar
diff --git a/Tests.lean b/Tests.lean
index 694e342..ff626a2 100644
--- a/Tests.lean
+++ b/Tests.lean
@@ -62,6 +62,14 @@ def cases : List TestCase := [
     .okTyNorm (.id .nat .zero .zero) .refl⟩,
   ⟨"idElim computes on refl",    Examples.idElimNat,
     .okTyNorm .nat .zero⟩,
+  ⟨"transport combinator typechecks", Examples.transportNat,
+    .okTy (.pi .nat (.pi .nat (.pi (.id .nat (.var 1) (.var 0)) (.pi .nat .nat))))⟩,
+  ⟨"transport computes on refl", Examples.transportNatRefl,
+    .okTyNorm .nat (.succ (.succ .zero))⟩,
+  ⟨"congruence combinator typechecks", Examples.congSucc,
+    .okTy (.pi .nat (.pi .nat (.pi (.id .nat (.var 1) (.var 0)) (.id .nat (.succ (.var 2)) (.succ (.var 1))))))⟩,
+  ⟨"congruence computes on refl", Examples.congSuccRefl,
+    .okTyNorm (.id .nat (.succ .zero) (.succ .zero)) .refl⟩,
   ⟨"fst infers the first projection", Examples.fstDepPair,
     .okTy (.univ 2)⟩,
   ⟨"snd infers the dependent second projection", Examples.sndDepPair,