Merge branch 'main' of https://gitlab.eecs.umich.edu/gradual-typing/sgdt

formalizations/guarded-cubical/ErrorDomains.agda

@@ -128,27 +128,21 @@ trivialize2 {X} _R_ hSym hTrans hCong hθ = fix trivialize2'
 -- (θ (next (fix θ)))  R
 -- (fix θ)
 
--- alternatively, we can drop symmetry if we assume that the relation
+-- don't need symmetry
 trivialize3 : {X : Type} (_R_ : L℧ X -> L℧ X -> Type) ->
   transitive _R_ ->
   congruence _R_ ->
-  congruence _R_ ->
   ((x : L℧ X) -> x R (θ (next x))) ->
   ((x : L℧ X) -> x R (fix θ))
- 
+trivialize3 {X} _R_ hTrans hCong hθR = fix trivialize3'
   where
-  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 =
-   trivialize3' IH lx =
-     hTrans
+     subst (λ y → lx R y) (sym (fix-eq θ))
        (hTrans
- 
-         (hCong (λ t → IH t lx))
+         (hθR lx)
+         (hCong (λ t → IH t lx)))
 
 --------------------------------------------------------------------------