Add dependent sums.

1 files changed, 14 insertions, 0 deletions

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index 90616d4..ef90cb8 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -36,6 +36,20 @@ abstractSyntax ctx (App t u) = do
   t <- abstractSyntax ctx t
   u <- abstractSyntax ctx u
   pure (App t u)
+abstractSyntax ctx (Sigma bounds var a b) = do
+  a <- abstractSyntax ctx a
+  b <- abstractSyntax (bind ctx var.val) b
+  pure (Sigma bounds var.val a b)
+abstractSyntax ctx (Pair b t u) = do
+  t <- abstractSyntax ctx t
+  u <- abstractSyntax ctx u
+  pure (Pair b t u)
+abstractSyntax ctx (Fst b t) = do
+  t <- abstractSyntax ctx t
+  pure (Fst b t)
+abstractSyntax ctx (Snd b t) = do
+  t <- abstractSyntax ctx t
+  pure (Snd b t)
 abstractSyntax ctx (Top b) = pure (Top b)
 abstractSyntax ctx (Point b) = pure (Point b)
 abstractSyntax ctx (Bottom b) = pure (Bottom b)