From 8eae3d8348a5bfceba23b0c4c0c4c66263ece522 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Sun, 8 Oct 2023 09:58:59 -0400
Subject: [PATCH] implement the end-to-end monad normalization function

---
 formalizations/guarded-cubical/Syntax/Normalization.agda | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/formalizations/guarded-cubical/Syntax/Normalization.agda b/formalizations/guarded-cubical/Syntax/Normalization.agda
index 57297c3..df2c00a 100644
--- a/formalizations/guarded-cubical/Syntax/Normalization.agda
+++ b/formalizations/guarded-cubical/Syntax/Normalization.agda
@@ -239,3 +239,10 @@ cases .indbind {M = M} = rec (isPropΠ λ _ → squash₁) λ ihN[x] ihM →
 
 readOut : ∥ fiber unCNfm M ∥₁ → singl M
 readOut = rec isPropSingl (λ x → (unCNfm (x .fst)) , (sym (x .snd)))
+
+csimpl : Comp Γ R → Comp Γ R
+csimpl M = fst (readOut (Sem.indPc cases M))
+
+csimpl-eq : (M : Comp Γ R) → M ≡ csimpl M
+csimpl-eq M = snd (readOut (Sem.indPc cases M))
+
-- 
GitLab