diff --git a/0Trinitarianism/Quest3.agda b/0Trinitarianism/Quest3.agda
index 151d6be..0df6b51 100644
--- a/0Trinitarianism/Quest3.agda
+++ b/0Trinitarianism/Quest3.agda
@@ -5,5 +5,7 @@ open import 0Trinitarianism.Preambles.P3
 _+_ : ℕ → ℕ → ℕ
 n + m = {!!}
 
-SumOfEven : (x : Σ ℕ isEven) → (y : Σ ℕ isEven) → isEven (x .fst + y .fst)
-SumOfEven x y = {!!}
+{-
+Write here you proof that the sum of
+even naturals is even.
+-}
diff --git a/0Trinitarianism/Quest3Solutions.agda b/0Trinitarianism/Quest3Solutions.agda
index 8798ce0..c99b543 100644
--- a/0Trinitarianism/Quest3Solutions.agda
+++ b/0Trinitarianism/Quest3Solutions.agda
@@ -10,13 +10,13 @@ _+'_ : ℕ → ℕ → ℕ
 zero +' n = n
 suc m +' n = suc (m +' n)
 
-SumOfEven : (x : Σ ℕ isEven) → (y : Σ ℕ isEven) → isEven (x .fst + y .fst)
+SumOfEven : (x y : Σ ℕ isEven) → isEven (x .fst + y .fst)
 SumOfEven x (zero , hy) = x .snd
 SumOfEven x (suc (suc y) , hy) = SumOfEven x (y , hy)
 
 {-
 
-Sum'OfEven : (x : Σ ℕ isEven) → (y : Σ ℕ isEven) → isEven (x .fst +' y .fst)
+Sum'OfEven : (x y : Σ ℕ isEven) → isEven (x .fst +' y .fst)
 Sum'OfEven x (zero , hy) = x .snd
 Sum'OfEven x (suc (suc y) , hy) = Sum'OfEven x (y , hy)
 
diff --git a/1FundamentalGroup/Preambles/P2.agda b/1FundamentalGroup/Preambles/P2.agda
index d26c358..6f027da 100644
--- a/1FundamentalGroup/Preambles/P2.agda
+++ b/1FundamentalGroup/Preambles/P2.agda
@@ -2,7 +2,7 @@ module 1FundamentalGroup.Preambles.P2 where
 
 open import Cubical.Data.Nat public
 open import Cubical.Data.Int using (ℤ ; pos ; negsuc ; -_) public
-open import Cubical.Foundations.Isomorphism public
+open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_) public
 open import Cubical.Foundations.Prelude renaming (subst to endPt) public
 open import Cubical.HITs.S1 using (S¹ ; base ; loop) public
 open import 1FundamentalGroup.Quest1Solutions public
diff --git a/1FundamentalGroup/Quest2Solutions.agda b/1FundamentalGroup/Quest2Solutions.agda
index 0ae8831..1a828fb 100644
--- a/1FundamentalGroup/Quest2Solutions.agda
+++ b/1FundamentalGroup/Quest2Solutions.agda
@@ -12,7 +12,7 @@ predℤ (pos zero) = negsuc zero
 predℤ (pos (suc n)) = pos n
 predℤ (negsuc n) = negsuc (suc n)
 
-sucℤIso : Iso ℤ ℤ
+sucℤIso : ℤ ≅ ℤ
 sucℤIso = iso sucℤ predℤ s r where
 
   s : section sucℤ predℤ
diff --git a/_build/2.6.2/agda/0Trinitarianism/Preambles/P3.agdai b/_build/2.6.2/agda/0Trinitarianism/Preambles/P3.agdai
new file mode 100644
index 0000000..78d275a
Binary files /dev/null and b/_build/2.6.2/agda/0Trinitarianism/Preambles/P3.agdai differ
diff --git a/_build/2.6.2/agda/0Trinitarianism/Quest3Solutions.agdai b/_build/2.6.2/agda/0Trinitarianism/Quest3Solutions.agdai
new file mode 100644
index 0000000..5cfb7a3
Binary files /dev/null and b/_build/2.6.2/agda/0Trinitarianism/Quest3Solutions.agdai differ
diff --git a/_build/2.6.2/agda/1FundamentalGroup/Preambles/P2.agdai b/_build/2.6.2/agda/1FundamentalGroup/Preambles/P2.agdai
index c54b7bf..4dc91c7 100644
Binary files a/_build/2.6.2/agda/1FundamentalGroup/Preambles/P2.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Preambles/P2.agdai differ
diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest2Solutions.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest2Solutions.agdai
index cf233b9..26aa13f 100644
Binary files a/_build/2.6.2/agda/1FundamentalGroup/Quest2Solutions.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Quest2Solutions.agdai differ