From b4d42a94342c992dbdac835250bd341581e87cee Mon Sep 17 00:00:00 2001
From: flupe <lucas@escot.me>
Date: Wed, 17 Jan 2024 17:03:12 +0100
Subject: [PATCH] fix translation of pi

---
 app/Agda/Core/ToCore.hs | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/app/Agda/Core/ToCore.hs b/app/Agda/Core/ToCore.hs
index b66372d..bafb438 100644
--- a/app/Agda/Core/ToCore.hs
+++ b/app/Agda/Core/ToCore.hs
@@ -122,10 +122,11 @@ instance ToCore I.Term where
 
   toCore I.Con{} = throwError "cubical endpoint application to constructors not supported"
 
-  toCore (I.Pi dom codom) = TPi <$> toCore dom <*> toCore codom
-        -- NOTE(flupe): we will need the sorts in the core syntax soon
-        -- <$> toCore (dom   .^ lensSort)
-        -- <*> toCore (codom .^ lensSort)
+  toCore (I.Pi dom codom) =
+    TPi <$> toCore (dom           ^. lensSort)
+        <*> toCore (absBody codom ^. lensSort)
+        <*> toCore dom
+        <*> toCore codom
 
   toCore (I.Sort s) = TSort <$> toCore s