From 99f4a00658e402ecd9595a17d0accaa4f483de28 Mon Sep 17 00:00:00 2001
From: Eric Giovannini <ecg19@seas.upenn.edu>
Date: Tue, 24 Oct 2023 02:57:55 +0100
Subject: [PATCH] Update translation from surface to intensional

---
 formalizations/guarded-cubical/Syntax/Translation.agda | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/formalizations/guarded-cubical/Syntax/Translation.agda b/formalizations/guarded-cubical/Syntax/Translation.agda
index dcbe438..684efcb 100644
--- a/formalizations/guarded-cubical/Syntax/Translation.agda
+++ b/formalizations/guarded-cubical/Syntax/Translation.agda
@@ -15,6 +15,7 @@ open import Cubical.Data.Sigma
 open import Syntax.Types
 open import Syntax.Surface
 open import Syntax.IntensionalTerms
+open import Syntax.IntensionalOrder
 open import Syntax.SyntacticBisimilarity
 
 open TyPrec
@@ -42,8 +43,8 @@ var-to-val (vs {T = T} x) = (var-to-val x) [ wk ]v
 ι (lda M) = ret' (lda (ι M))
 ι (app M N) = app'' (ι M) (ι N)
 ι err = err'
-ι (up S⊑T M) = (upE S⊑T [ !s ]e) [ ι M ]∙
-ι (dn S⊑T M) = (dn S⊑T [ !s ]e) [ ι M ]∙
+ι (up S⊑T M) = {!!} -- (upE S⊑T [ !s ]e) [ ι M ]∙
+ι (dn S⊑T M) = {!!} -- (dn S⊑T [ !s ]e) [ ι M ]∙
 ι zro = ret' zro'
 ι (suc M) = (ι M) >> (ret' (suc' var)) -- (bind (ret' (suc' var))) [ ι M ]∙
 ι (matchNat M Kz Ks) = {!!}
-- 
GitLab