diff --git a/hott/algebra/field.hlean b/hott/algebra/field.hlean
index a74dceddf..298aeb112 100644
--- a/hott/algebra/field.hlean
+++ b/hott/algebra/field.hlean
@@ -3,7 +3,7 @@ Copyright (c) 2014 Robert Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis
 
-Structures with multiplicative prod additive components, including division rings prod fields.
+Structures with multiplicative and additive components, including division rings and fields.
 The development is modeled after Isabelle's library.
 -/
 import algebra.binary algebra.group algebra.ring
@@ -325,7 +325,7 @@ section discrete_field
   variables {a b c d : A}
 
   -- many of the theorems in discrete_field are the same as theorems in field sum division ring,
-  -- but with fewer hypotheses since 0⁻¹ = 0 prod equality is decidable.
+  -- but with fewer hypotheses since 0⁻¹ = 0 and equality is decidable.
 
   theorem discrete_field.eq_zero_sum_eq_zero_of_mul_eq_zero
     (x y : A) (H : x * y = 0) : x = 0 ⊎ y = 0 :=
diff --git a/hott/algebra/order.hlean b/hott/algebra/order.hlean
index 21f2e39ec..c16a48286 100644
--- a/hott/algebra/order.hlean
+++ b/hott/algebra/order.hlean
@@ -3,7 +3,7 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Jeremy Avigad
 
-Weak orders "≤", strict orders "<", prod structures that include both.
+Weak orders "≤", strict orders "<", and structures that include both.
 -/
 import algebra.binary algebra.priority
 open eq eq.ops algebra
@@ -85,7 +85,7 @@ definition wf.rec_on {A : Type} [s : wf_strict_order A] {P : A → Type}
     (x : A) (H : Πx, (Πy, wf_strict_order.lt y x → P y) → P x) : P x :=
 wf_strict_order.wf_rec P H x
 
-/- structures with a weak prod a strict order -/
+/- structures with a weak and a strict order -/
 
 structure order_pair [class] (A : Type) extends weak_order A, has_lt A :=
 (le_of_lt : Π a b, lt a b → le a b)
@@ -304,7 +304,7 @@ section
   definition min (a b : A) : A := if a ≤ b then a else b
   definition max (a b : A) : A := if a ≤ b then b else a
 
-  /- these show min prod max form a lattice -/
+  /- these show min and max form a lattice -/
 
   theorem min_le_left (a b : A) : min a b ≤ a :=
   by_cases
@@ -342,7 +342,7 @@ section
   theorem le_max_right_iff_unit (a b : A) : b ≤ max a b ↔ unit :=
   iff_unit_intro (le_max_right a b)
 
-  /- these are also proved for lattices, but with inf prod sup in place of min prod max -/
+  /- these are also proved for lattices, but with inf and sup in place of min and max -/
 
   theorem eq_min {a b c : A} (H₁ : c ≤ a) (H₂ : c ≤ b) (H₃ : Π{d}, d ≤ a → d ≤ b → d ≤ c) :
     c = min a b :=
diff --git a/hott/algebra/ordered_ring.hlean b/hott/algebra/ordered_ring.hlean
index f3e77e0e8..55605590d 100644
--- a/hott/algebra/ordered_ring.hlean
+++ b/hott/algebra/ordered_ring.hlean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
 
 Here an "ordered_ring" is partially ordered ring, which is ordered with respect to both a weak
-order prod an associated strict order. Our numeric structures (int, rat, prod real) will be instances
+order and an associated strict order. Our numeric structures (int, rat, and real) will be instances
 of "linear_ordered_comm_ring". This development is modeled after Isabelle's library.
 -/
 
@@ -711,7 +711,7 @@ section
 
 end
 
-/- TODO: Multiplication prod one, starting with mult_right_le_one_le. -/
+/- TODO: Multiplication and one, starting with mult_right_le_one_le. -/
 
 namespace norm_num
 
diff --git a/hott/algebra/port.md b/hott/algebra/port.md
index 3a132cd26..db5b75e57 100644
--- a/hott/algebra/port.md
+++ b/hott/algebra/port.md
@@ -6,4 +6,6 @@ Port instructions:
 - All of the algebraic hierarchy is in the algebra namespace in the HoTT library.
 - Open namespaces `eq` and `algebra` if needed
 - (optional) add option `set_option class.force_new true`
-- fix all remaining errors
+- fix all remaining errors. Typical errors include
+  - Replacing "and" by "prod" in comments
+  - and.intro is replaced by prod.intro, which should be prod.mk.
diff --git a/hott/algebra/ring.hlean b/hott/algebra/ring.hlean
index 924c3d450..faf112e86 100644
--- a/hott/algebra/ring.hlean
+++ b/hott/algebra/ring.hlean
@@ -3,7 +3,7 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura
 
-Structures with multiplicative prod additive components, including semirings, rings, prod fields.
+Structures with multiplicative and additive components, including semirings, rings, and fields.
 The development is modeled after Isabelle's library.
 -/
 
@@ -384,7 +384,7 @@ section
   assert a * a = 1 * 1 ↔ a = 1 ⊎ a = -1, from mul_self_eq_mul_self_iff a 1,
   by rewrite mul_one at this; exact this
 
-  -- TODO: c - b * c → c = 0 ⊎ b = 1 prod variants
+  -- TODO: c - b * c → c = 0 ⊎ b = 1 and variants
 
   theorem dvd_of_mul_dvd_mul_left {a b c : A} (Ha : a ≠ 0) (Hdvd : (a * b ∣ a * c)) : (b ∣ c) :=
   dvd.elim Hdvd
diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean
index 3998ccdf8..387f2b618 100644
--- a/hott/init/logic.hlean
+++ b/hott/init/logic.hlean
@@ -663,7 +663,7 @@ theorem if_simp_congr_prop [congr] {b c x y u v : Type} [dec_b : decidable b]
         ite b x y ↔ (@ite c (decidable_of_decidable_of_iff dec_b h_c) Type u v) :=
 @if_ctx_simp_congr_prop b c x y u v dec_b h_c (λ h, h_t) (λ h, h_e)
 
--- Remark: dite prod ite are "definitionally equal" when we ignore the proofs.
+-- Remark: dite and ite are "definitionally equal" when we ignore the proofs.
 theorem dite_ite_eq (c : Type) [H : decidable c] {A : Type} (t : A) (e : A) : dite c (λh, t) (λh, e) = ite c t e :=
 rfl
 
diff --git a/hott/types/int/basic.hlean b/hott/types/int/basic.hlean
index 0d1a1b4f9..c004028b6 100644
--- a/hott/types/int/basic.hlean
+++ b/hott/types/int/basic.hlean
@@ -3,11 +3,11 @@ Copyright (c) 2014 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Jeremy Avigad
 
-The integers, with addition, multiplication, prod subtraction. The representation of the integers is
+The integers, with addition, multiplication, and subtraction. The representation of the integers is
 chosen to compute efficiently.
 
 To faciliate proving things about these operations, we show that the integers are a quotient of
-ℕ × ℕ with the usual equivalence relation, ≡, prod functions
+ℕ × ℕ with the usual equivalence relation, ≡, and functions
 
   abstr : ℕ × ℕ → ℤ
   repr : ℤ → ℕ × ℕ
@@ -69,7 +69,7 @@ definition neg_of_nat : ℕ → ℤ
 definition sub_nat_nat (m n : ℕ) : ℤ :=
 match (n - m : nat) with
   | 0        := of_nat (m - n)  -- m ≥ n
-  | (succ k) := -[1+ k]         -- m < n, prod n - m = succ k
+  | (succ k) := -[1+ k]         -- m < n, and n - m = succ k
 end
 
 protected definition neg (a : ℤ) : ℤ :=
@@ -105,7 +105,7 @@ rfl
 lemma mul_neg_succ_of_nat_neg_succ_of_nat (m n : nat) : -[1+ m] * -[1+ n] = succ m * succ n :=
 rfl
 
-/- some basic functions prod properties -/
+/- some basic functions and properties -/
 
 theorem of_nat.inj {m n : ℕ} (H : of_nat m = of_nat n) : m = n :=
 down (int.no_confusion H imp.id)
@@ -199,7 +199,7 @@ sum.elim (@le_sum_gt _ _ (pr2 p) (pr1 p))
 
 protected theorem equiv_of_eq {p q : ℕ × ℕ} (H : p = q) : p ≡ q := H ▸ equiv.refl
 
-/- the representation prod abstraction functions -/
+/- the representation and abstraction functions -/
 
 definition abstr (a : ℕ × ℕ) : ℤ := sub_nat_nat (pr1 a) (pr2 a)
 
diff --git a/hott/types/nat/basic.hlean b/hott/types/nat/basic.hlean
index 845c304f6..84da93050 100644
--- a/hott/types/nat/basic.hlean
+++ b/hott/types/nat/basic.hlean
@@ -43,7 +43,7 @@ nat.rec_on x
                    ...  = succ (succ x₁ ⊕ y₁) : {ih₂}
                    ...  = succ x₁ ⊕ succ y₁   : addl_succ_right))
 
-/- successor prod predecessor -/
+/- successor and predecessor -/
 
 theorem succ_ne_zero (n : ℕ) : succ n ≠ 0 :=
 by contradiction
diff --git a/hott/types/nat/order.hlean b/hott/types/nat/order.hlean
index f6c1099f1..eec658419 100644
--- a/hott/types/nat/order.hlean
+++ b/hott/types/nat/order.hlean
@@ -10,7 +10,7 @@ open eq eq.ops algebra algebra
 
 namespace nat
 
-/- lt prod le -/
+/- lt and le -/
 
 protected theorem le_of_lt_sum_eq {m n : ℕ} (H : m < n ⊎ m = n) : m ≤ n :=
 nat.le_of_eq_sum_lt (sum.swap H)
@@ -88,7 +88,7 @@ nat.lt_of_lt_of_le (nat.lt_add_of_pos_right Hk) (!mul_succ ▸ nat.mul_le_mul_le
 protected theorem mul_lt_mul_of_pos_right {n m k : ℕ} (H : n < m) (Hk : k > 0) : n * k < m * k :=
 !mul.comm ▸ !mul.comm ▸ nat.mul_lt_mul_of_pos_left H Hk
 
-/- nat is an instance of a linearly ordered semiring prod a lattice -/
+/- nat is an instance of a linearly ordered semiring and a lattice -/
 
 protected definition decidable_linear_ordered_semiring [reducible] [trans_instance] :
 decidable_linear_ordered_semiring nat :=
@@ -172,7 +172,7 @@ theorem eq_zero_of_le_zero {n : ℕ} (H : n ≤ 0) : n = 0 :=
 obtain (k : ℕ) (Hk : n + k = 0), from le.elim H,
 eq_zero_of_add_eq_zero_right Hk
 
-/- succ prod pred -/
+/- succ and pred -/
 
 theorem le_of_lt_succ {m n : nat} : m < succ n → m ≤ n :=
 le_of_succ_le_succ
@@ -332,7 +332,7 @@ dvd.elim H
   (take m, suppose 1 = n * m,
    eq_one_of_mul_eq_one_right this⁻¹)
 
-/- min prod max -/
+/- min and max -/
 open decidable
 
 theorem min_zero [simp] (a : ℕ) : min a 0 = 0 :=
@@ -386,7 +386,7 @@ decidable.by_cases
 protected theorem max_add_add_right (a b c : ℕ) : max (a + c) (b + c) = max a b + c :=
 by rewrite [add.comm a c, add.comm b c, add.comm _ c]; apply nat.max_add_add_left
 
-/- least prod greatest -/
+/- least and greatest -/
 
 section least_prod_greatest
   variable (P : ℕ → Type)
diff --git a/hott/types/nat/sub.hlean b/hott/types/nat/sub.hlean
index cb341088d..74bc20588 100644
--- a/hott/types/nat/sub.hlean
+++ b/hott/types/nat/sub.hlean
@@ -3,7 +3,7 @@ Copyright (c) 2014 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Authors: Floris van Doorn, Jeremy Avigad
-Subtraction on the natural numbers, as well as min, max, prod distance.
+Subtraction on the natural numbers, as well as min, max, and distance.
 -/
 import .order
 open eq.ops algebra eq
diff --git a/script/port.pl b/script/port.pl
index a82d3d933..69ed1edb2 100755
--- a/script/port.pl
+++ b/script/port.pl
@@ -18,6 +18,10 @@
 # We use slightly different regular expressions here. Given the replacement rule foo:bar, we replace
 # foo by bar except is foo is preceded or followed by a letter. We still replace foo if it's
 # followed by a digit, underscore, period or similar.
+#
+# TODO: Currently we use dictionaries to store the renamings. This has the unfortunate consequence
+# that we cannot control the order in which the substitutions happens. This makes it very hard to
+# replace all occurrences of "and" by "prod", but all occurrences of "and.intro" by "prod.mk"
 
 use strict;
 use warnings;