From 8e0d6e6ee4ac23dc37bf71251fd70fa6ebe3d441 Mon Sep 17 00:00:00 2001
From: =?utf8?q?Anders=20M=C3=B6rtberg?= <andersmortberg@gmail.com>
Date: Mon, 20 Nov 2017 18:46:37 -0500
Subject: [PATCH] simplify more

---
 examples/univalence.ctt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/examples/univalence.ctt b/examples/univalence.ctt
index a8f0e0e..b015cef 100644
--- a/examples/univalence.ctt
+++ b/examples/univalence.ctt
@@ -219,7 +219,7 @@ uabeta (A B : U) (e : equiv A B) : Path (A -> B) (trans A B (ua A B e)) e.1 =
 uaret (A B : U) : retract (equiv A B) (Path U A B) (ua A B) (transEquiv A B) =
   \(e : equiv A B) ->
   let rem (a : A) : Path B ((transEquiv A B (ua A B e)).1 a) (e.1 a) =
-        <i> fill (<_> B) (fill (<_> B) (e.1 (fill (<_> A) a [] @ -i)) [] @ -i) [] @ -i
+        <i> (uabeta A B e @ i) (fill (<_> A) a [] @ -i)
   in equivLemma A B (transEquiv A B (ua A B e)) e (<i> \(a : A) -> rem a @ i)
 
 -- So  (B:U) x equiv A B    is a retract of    (B:U) x Path U A B
-- 
2.34.1