diff --git a/0Trinitarianism/Quest4Solutions.agda b/0Trinitarianism/Quest4Solutions.agda
index 020e198..af45d3f 100644
--- a/0Trinitarianism/Quest4Solutions.agda
+++ b/0Trinitarianism/Quest4Solutions.agda
@@ -1,6 +1,6 @@
 module 0Trinitarianism.Quest4Solutions where
 
-open import Cubical.Foundations.Prelude using ( Level ; Type ; _≡_ ; J ; JRefl ; refl )
+open import Cubical.Foundations.Prelude using ( Level ; Type ; _≡_ ; J ; JRefl ; refl ; i1 ; i0 ; I)
 open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_)
 
 infixr 30 _∙_
@@ -184,7 +184,6 @@ endPtRefl {x = x} B = JRefl ((λ y p → B x → B y)) id
 endPt' : (B : A → Type) (p : x ≡ y) → B x → B y
 endPt' B p = pathToFun (Cubical.Foundations.Prelude.cong B p )
 
-
 --------------funExt---------------------
 
 funExt : (B : A → Type) (f g : (a : A) → B a) →
diff --git a/_build/2.6.2/agda/0Trinitarianism/Quest4Solutions.agdai b/_build/2.6.2/agda/0Trinitarianism/Quest4Solutions.agdai
index a368964..83dfe40 100644
Binary files a/_build/2.6.2/agda/0Trinitarianism/Quest4Solutions.agdai and b/_build/2.6.2/agda/0Trinitarianism/Quest4Solutions.agdai differ