diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index c57e183..37c760f 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -10,13 +10,15 @@ open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
 open import Cat.Category
 open import Cat.Functor
 
+-- Tip from Andrea:
 -- Use co-patterns - they help with showing more understandable types in goals.
 lift-eq : ∀ {ℓ} {A B : Set ℓ} {a a' : A} {b b' : B} → a ≡ a' → b ≡ b' → (a , b) ≡ (a' , b')
 fst (lift-eq a b i) = a i
 snd (lift-eq a b i) = b i
---lift-eq a b = λ i → a i , b i
-
 
+eqpair : ∀ {ℓa ℓb} {A : Set ℓa} {B : Set ℓb} {a a' : A} {b b' : B}
+  → a ≡ a' → b ≡ b' → (a , b) ≡ (a' , b')
+eqpair eqa eqb i = eqa i , eqb i
 
 open Functor
 open Category
diff --git a/src/Cat/Category/Free.agda b/src/Cat/Category/Free.agda
index 98305a6..ff06743 100644
--- a/src/Cat/Category/Free.agda
+++ b/src/Cat/Category/Free.agda
@@ -11,12 +11,10 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
     open module ℂ = Category ℂ
     Obj = ℂ.Object
 
-  Path : ( a b : Obj ) → Set ℓ'
-  Path a b = undefined
-
-  postulate emptyPath : (o : Obj) → Path o o
-
-  postulate concatenate : {a b c : Obj} → Path b c → Path a b → Path a c
+  postulate
+    Path : ( a b : Obj ) → Set ℓ'
+    emptyPath : (o : Obj) → Path o o
+    concatenate : {a b c : Obj} → Path b c → Path a b → Path a c
 
   private
     module _ {A B C D : Obj} {r : Path A B} {q : Path B C} {p : Path C D} where