From a353946b7a75ded89900a3457698b5c5f9fc351d Mon Sep 17 00:00:00 2001
From: Eric Giovannini <ecg19@seas.upenn.edu>
Date: Tue, 11 Oct 2022 21:35:42 -0400
Subject: [PATCH] fix merge issue

---
 formalizations/guarded-cubical/ErrorDomains.agda | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

diff --git a/formalizations/guarded-cubical/ErrorDomains.agda b/formalizations/guarded-cubical/ErrorDomains.agda
index a1b7ad4..c278d82 100644
--- a/formalizations/guarded-cubical/ErrorDomains.agda
+++ b/formalizations/guarded-cubical/ErrorDomains.agda
@@ -128,21 +128,27 @@ trivialize2 {X} _R_ hSym hTrans hCong hθ = fix trivialize2'
 -- (θ (next (fix θ)))  R
 -- (fix θ)
 
--- don't need symmetry
+-- alternatively, we can drop symmetry if we assume that the relation
+-- is reflexive, or at least that fix θ is related to itself.
 trivialize3 : {X : Type} (_R_ : L℧ X -> L℧ X -> Type) ->
   transitive _R_ ->
   congruence _R_ ->
+  fix θ R fix θ ->
   ((x : L℧ X) -> x R (θ (next x))) ->
   ((x : L℧ X) -> x R (fix θ))
-trivialize3 {X} _R_ hTrans hCong hθR = fix trivialize3'
+trivialize3 {X} _R_ hTrans hCong fix-ok hθR = fix trivialize3'
   where
+   lem : θ (next (fix θ)) R fix θ
+   lem = subst (λ x → x R fix θ) (fix-eq θ) fix-ok
+
    trivialize3' :
     ▹ ((x : L℧ X) -> x R (fix θ)) → (x : L℧ X) -> x R (fix θ)
    trivialize3' IH lx =
-     subst (λ y → lx R y) (sym (fix-eq θ))
+     hTrans
+       (hθR lx)
        (hTrans
-         (hθR lx)
-         (hCong (λ t → IH t lx)))
+         (hCong (λ t → IH t lx))
+         lem)
 
 --------------------------------------------------------------------------
 
-- 
GitLab