diff --git a/1FundamentalGroup/Preambles/P0.agda b/1FundamentalGroup/Preambles/P0.agda
index 4dc19c6..13e74e3 100644
--- a/1FundamentalGroup/Preambles/P0.agda
+++ b/1FundamentalGroup/Preambles/P0.agda
@@ -3,7 +3,10 @@ module 1FundamentalGroup.Preambles.P0 where
 open import Cubical.Data.Empty using (⊥) public
 open import Cubical.Data.Unit renaming ( Unit to ⊤ ) public
 open import Cubical.Data.Bool public
-open import Cubical.Foundations.Prelude renaming ( subst to endPt ) public
+open import Cubical.Foundations.Prelude
+     renaming ( subst to endPt
+              ; transport to pathToFun
+              ) public
 open import Cubical.Foundations.Isomorphism renaming ( Iso to _≅_ ) public
 open import Cubical.Foundations.Path public
 open import Cubical.HITs.S1 public
diff --git a/1FundamentalGroup/Preambles/P1.agda b/1FundamentalGroup/Preambles/P1.agda
index 23c3d31..0c9c2a7 100644
--- a/1FundamentalGroup/Preambles/P1.agda
+++ b/1FundamentalGroup/Preambles/P1.agda
@@ -4,6 +4,9 @@ open import Cubical.HITs.S1 using (S¹ ; base ; loop) public
 open import Cubical.Data.Nat using (ℕ ; suc ; zero) public
 open import Cubical.Data.Int using (ℤ ; pos ; negsuc ; -_) public
 open import Cubical.Data.Empty public
-open import Cubical.Foundations.Prelude renaming (subst to endPt) public
+open import Cubical.Foundations.Prelude
+     renaming ( subst to endPt
+              ; transport to pathToFun
+              ) public
 open import Cubical.Foundations.Isomorphism renaming (Iso to _≅_) public
 open import 1FundamentalGroup.Quest0Solutions using ( Refl ; Refl≢loop ) public
diff --git a/1FundamentalGroup/Preambles/P2.agda b/1FundamentalGroup/Preambles/P2.agda
index 6f027da..83a8993 100644
--- a/1FundamentalGroup/Preambles/P2.agda
+++ b/1FundamentalGroup/Preambles/P2.agda
@@ -3,6 +3,9 @@ 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 renaming (Iso to _≅_) public
-open import Cubical.Foundations.Prelude renaming (subst to endPt) public
+open import Cubical.Foundations.Prelude
+     renaming ( subst to endPt
+              ; transport to pathToFun
+              ) public
 open import Cubical.HITs.S1 using (S¹ ; base ; loop) public
 open import 1FundamentalGroup.Quest1Solutions public
diff --git a/1FundamentalGroup/Quest0Solutions.agda b/1FundamentalGroup/Quest0Solutions.agda
index de9b7ea..2002e49 100644
--- a/1FundamentalGroup/Quest0Solutions.agda
+++ b/1FundamentalGroup/Quest0Solutions.agda
@@ -61,12 +61,12 @@ isoEmpty→pathEmpty : (A : Type) → isoEmpty A → pathEmpty A
 isoEmpty→pathEmpty A = isoToPath
 
 pathEmpty→toEmpty : (A : Type) → pathEmpty A → toEmpty A
-pathEmpty→toEmpty A p x = transport p x
+pathEmpty→toEmpty A p x = pathToFun p x
 
 ------------------- Side Quests - true≢false --------------------
 
 true≢false' : true ≡ false → ⊥
-true≢false' h = transport ⊤≡⊥ tt where
+true≢false' h = pathToFun ⊤≡⊥ tt where
 
   propify : Bool → Type
   propify false = ⊥
diff --git a/1FundamentalGroup/Quest2Solutions.agda b/1FundamentalGroup/Quest2Solutions.agda
index 1a828fb..45df76b 100644
--- a/1FundamentalGroup/Quest2Solutions.agda
+++ b/1FundamentalGroup/Quest2Solutions.agda
@@ -2,40 +2,40 @@
 module 1FundamentalGroup.Quest2Solutions where
 open import 1FundamentalGroup.Preambles.P2
 
-sucℤ : ℤ → ℤ
-sucℤ (pos n) = pos (suc n)
-sucℤ (negsuc zero) = pos zero
-sucℤ (negsuc (suc n)) = negsuc n
+-- sucℤ : ℤ → ℤ
+-- sucℤ (pos n) = pos (suc n)
+-- sucℤ (negsuc zero) = pos zero
+-- sucℤ (negsuc (suc n)) = negsuc n
 
-predℤ : ℤ → ℤ
-predℤ (pos zero) = negsuc zero
-predℤ (pos (suc n)) = pos n
-predℤ (negsuc n) = negsuc (suc n)
+-- predℤ : ℤ → ℤ
+-- predℤ (pos zero) = negsuc zero
+-- predℤ (pos (suc n)) = pos n
+-- predℤ (negsuc n) = negsuc (suc n)
 
-sucℤIso : ℤ ≅ ℤ
-sucℤIso = iso sucℤ predℤ s r where
+-- sucℤIso : ℤ ≅ ℤ
+-- sucℤIso = iso sucℤ predℤ s r where
 
-  s : section sucℤ predℤ
-  s (pos zero) = refl
-  s (pos (suc n)) = refl
-  s (negsuc zero) = refl
-  s (negsuc (suc n)) = refl
+--   s : section sucℤ predℤ
+--   s (pos zero) = refl
+--   s (pos (suc n)) = refl
+--   s (negsuc zero) = refl
+--   s (negsuc (suc n)) = refl
 
-  r : retract sucℤ predℤ
-  r (pos zero) = refl
-  r (pos (suc n)) = refl
-  r (negsuc zero) = refl
-  r (negsuc (suc n)) = refl
+--   r : retract sucℤ predℤ
+--   r (pos zero) = refl
+--   r (pos (suc n)) = refl
+--   r (negsuc zero) = refl
+--   r (negsuc (suc n)) = refl
 
-sucℤPath : ℤ ≡ ℤ
-sucℤPath = isoToPath sucℤIso
+-- sucℤPath : ℤ ≡ ℤ
+-- sucℤPath = isoToPath sucℤIso
 
-helix : S¹ → Type
-helix base = ℤ
-helix (loop i) = sucℤPath i
+-- helix : S¹ → Type
+-- helix base = ℤ
+-- helix (loop i) = sucℤPath i
 
-windingNumberBase : base ≡ base → ℤ
-windingNumberBase p = endPt helix p (pos zero)
+-- windingNumberBase : base ≡ base → ℤ
+-- windingNumberBase p = endPt helix p (pos zero)
 
-windingNumber : (x : S¹) → base ≡ x → helix x
-windingNumber x p = endPt helix p (pos zero)
+-- windingNumber : (x : S¹) → base ≡ x → helix x
+-- windingNumber x p = endPt helix p (pos zero)
diff --git a/_build/2.6.2/agda/1FundamentalGroup/Preambles/P0.agdai b/_build/2.6.2/agda/1FundamentalGroup/Preambles/P0.agdai
index cbed4c1..df9e748 100644
Binary files a/_build/2.6.2/agda/1FundamentalGroup/Preambles/P0.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Preambles/P0.agdai differ
diff --git a/_build/2.6.2/agda/1FundamentalGroup/Preambles/P1.agdai b/_build/2.6.2/agda/1FundamentalGroup/Preambles/P1.agdai
index f43097c..953d3b8 100644
Binary files a/_build/2.6.2/agda/1FundamentalGroup/Preambles/P1.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Preambles/P1.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 4dc91c7..82bcb23 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/Quest0Solutions.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest0Solutions.agdai
index 5b219a6..7e5baaf 100644
Binary files a/_build/2.6.2/agda/1FundamentalGroup/Quest0Solutions.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Quest0Solutions.agdai differ
diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest1Solutions.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest1Solutions.agdai
index 3dd2981..05f4f51 100644
Binary files a/_build/2.6.2/agda/1FundamentalGroup/Quest1Solutions.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Quest1Solutions.agdai differ
diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest2Solutions.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest2Solutions.agdai
index 26aa13f..38d8d90 100644
Binary files a/_build/2.6.2/agda/1FundamentalGroup/Quest2Solutions.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Quest2Solutions.agdai differ