diff --git a/src/ApPractice.agda b/src/ApPractice.agda
new file mode 100644
index 0000000..8dda84c
--- /dev/null
+++ b/src/ApPractice.agda
@@ -0,0 +1,58 @@
+module ApPractice where
+
+import Relation.Binary.PropositionalEquality as Eq
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) renaming (Set to Type) public
+open import Relation.Binary
+open import Relation.Binary.Indexed.Heterogeneous
+open import Relation.Binary.Core public
+open import Relation.Binary.Definitions public
+open import Relation.Binary.Structures public
+open import Relation.Binary.Bundles public
+open import Relation.Binary.PropositionalEquality.Core public
+open import Relation.Binary.PropositionalEquality.Properties public
+open import Relation.Binary.PropositionalEquality.Algebra public
+
+_∙_ = trans
+_∘_ : {A B C : Set} → (A → B) → (B → C) → A → C
+(f ∘ g) x = g (f x)
+
+ap : {A B : Set}
+  → (f : A → B)
+  → {x y : A}
+  → (p : x ≡ y)
+  → f x ≡ f y
+ap f {x} {x} refl = refl
+
+lemma222_i : {A B C : Set}
+  → (f : A → B)
+  → (g : B → C)
+  → {x y z : A}
+  → (p : x ≡ y)
+  → (q : y ≡ z)
+  → ap f (p ∙ q) ≡ ap f p ∙ ap f q
+lemma222_i f g refl refl = refl
+
+lemma222_ii : {A B C : Set}
+  → (f : A → B)
+  → {x y : A}
+  → (p : x ≡ y)
+  → ap f (sym p) ≡ sym (ap f p)
+lemma222_ii f refl = refl
+
+lemma222_iii : {A B C : Set}
+  → (f : A → B)
+  → (g : B → C)
+  → {x y z : A}
+  → (p : x ≡ y)
+  → (q : y ≡ z)
+  → ap g (ap f p) ≡ ap (f ∘ g) p
+lemma222_iii f g refl refl = refl
+
+id : {ℓ : Level} → {A : Set ℓ} → A → A
+id x = x
+
+lemma222_iv : {A : Set}
+  → {x y : A}
+  → (p : x ≡ y)
+  → ap id p ≡ p
+lemma222_iv p = refl
diff --git a/src/Ch6.agda b/src/Ch6.agda
index e0bc775..eb85954 100644
--- a/src/Ch6.agda
+++ b/src/Ch6.agda
@@ -55,7 +55,7 @@ lemma628 : {A : Type} (f g : S¹ → A)
   → (x : S¹)
   → f x ≡ g x
 lemma628 f g p q base = p
-lemma628 f g p q x = {! !} -- ICE: Try to split on x
+lemma628 f g p q (loop i) = ?
 -- f (loop i) = g (loop i)
 -- when i = i0
 --   f base = g base
diff --git a/src/Ch6HoTT.agda b/src/Ch6HoTT.agda
new file mode 100644
index 0000000..0342b94
--- /dev/null
+++ b/src/Ch6HoTT.agda
@@ -0,0 +1,112 @@
+{-# OPTIONS --without-K #-}
+
+module Ch6HoTT where
+
+-- S¹-ind : (P : S¹ → Set) → (b : P base) → (ℓ : transport loop b ≡ b) → (x : S¹) → P x
+-- S¹-ind P b ℓ base = transport ? b
+
+
+
+
+
+
+
+
+
+
+
+  -- f : A → B
+  -- a1 a2 : A
+  -- p : a1 ≡ a2
+  --
+  -- (ap f p) : f a1 ≡ f a2
+
+
+  -- f : (x : A) → B x
+  -- a1 a2 : A
+  -- p : a1 ≡ a2
+  --
+  -- T : B a1 → B a2
+  -- T = transport B p
+  -- (apd f p) : T (f a1) ≡ f a2
+  -- (apd f p) : transport B p (f a1) ≡ f a2
+
+import Relation.Binary.PropositionalEquality as Eq
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) renaming (Set to Type) public
+
+data _≡_ {l : Level} {A : Type l} : A → A → Type l where
+ refl : (x : A) → x ≡ x
+
+-- Path induction
+path-ind : ∀ {u} → {A : Set} → 
+          (C : (x y : A) → x ≡ y → Set u) → 
+          (c : (x : A) → C x x (refl x)) → 
+          {x y : A} → (p : x ≡ y) → C x y p
+path-ind C c {x} (refl x) = c x
+
+Path : {l : Level} (A : Type l) → A → A → Type l
+Path A x y = x ≡ y
+
+syntax Path A x y = x ≡ y [ A ]
+
+id : {ℓ : Level} {A : Set ℓ} → A → A
+id x = x
+
+-- Transport
+transport : {X : Set} (P : X → Set) {x y : X} → x ≡ y → P x → P y
+transport P (refl x) = id
+
+ap : {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
+ap f p = path-ind (λ x y p → f x ≡ f y) (λ x → ?) p
+
+postulate
+  S¹ : Set
+
+  base : S¹
+
+  loop : base ≡ base [ S¹ ]
+
+  -- (apd f p) : transport B p (f a1) ≡ f a2
+  -- apd _ loop
+  -- f : (x : A) → C x
+  -- loop : base ≡ base, base : S¹
+  --
+  -- apd f loop : transport C loop (f base) ≡ f base
+  --
+  -- S¹-ind : (C : S¹ → Set)
+  --   → (c-base : C base)
+  --   → (c-loop : ?)
+  --   → (s : S¹) → C s
+  --
+  -- N-ind : () → (c-zero : C 0) → ... → (n : N) → C n
+  --
+  -- N-ind 0 : C 0
+  --
+  -- f : (x : S¹) → C x
+  -- f = S¹-ind C _ _
+  --
+  -- f base : C base
+  --
+  -- apd (f) loop : (transport C loop (f base)) ≡ f base
+  -- (c-loop : (transport C loop (f base)) ≡ f base)
+  --
+  -- ap f (p₁ ∙ p₂) = (ap f p₁) ∙ (ap f p₂)
+
+-- (λ _ → A)
+
+lemma625 : {A : Set} → (a : A) → (p : a ≡ a) → (S¹ → A)
+lemma625 a p s1 = ?
+
+lemma625prop1 : {A : Set} {a : A} {p : a ≡ a} → (lemma625 a p base ≡ a)
+-- lemma625prop1 = refl
+
+lemma625prop2 : {A : Set} (a : A) → (p : a ≡ a) → ap (lemma625 a p) loop ≡ p
+-- lemma625prop2 a p = refl
+
+-- f : S¹ → A
+-- f = lemma625 a p
+--
+-- f-loop : f base ≡ f base
+-- f-loop : ap f loop
+--
+-- f-loop ≡ p