napkin solutions > HoTT
Back to Chapter Selection
Table of Contents
1.2
1.6
1.8
1.10
1.13
1.15
1.2
#
HoTT-1.2.
Derive the recursion principle for products
rec
𝐴
×
𝐵
using only the projections, and verify that
the definitional equalities are valid. Do the same for
Σ
-types.
Solution
by
RanolP
The exercise makes us define the recursor based on the projection of (maybe dependent) product types.
1.
rec
𝐴
×
𝐵
We have projections
•
pr
1
:
𝐴
×
𝐵
→
𝐴
•
pr
2
:
𝐴
×
𝐵
→
𝐵
with the following defining equations
•
pr
1
(
(
𝑎
,
𝑏
)
)
:
≡
𝑎
•
pr
2
(
(
𝑎
,
𝑏
)
)
:
≡
𝑏
Here, our goal is to define
rec
𝐴
×
𝐵
:
Π
𝐶
:
𝒰
(
𝐴
→
𝐵
→
𝐶
)
→
𝐴
×
𝐵
→
𝐶
and the definition is
rec
𝐴
×
𝐵
(
𝐶
,
𝑔
,
(
𝑎
,
𝑏
)
)
:
≡
𝑔
(
pr
1
(
(
𝑎
,
𝑏
)
)
)
(
pr
2
(
(
𝑎
,
𝑏
)
)
)
We can verify that the recursor above has the desired property by doing
𝛽
-reduction on
pr
1
and
pr
2
.
After the reduction, we get
𝑔
(
𝑎
)
(
𝑏
)
, correctly Church-encoding the product.
∎
2.
rec
Σ
𝑥
:
𝐴
𝐵
(
𝑥
)
We have projections
•
pr
1
:
(
Σ
𝑥
:
𝐴
𝐵
(
𝑥
)
)
→
𝐴
•
pr
2
:
Π
𝑝
:
Σ
(
𝑥
:
𝐴
)
𝐵
(
𝑥
)
𝐵
(
pr
1
(
𝑝
)
)
with the following defining equations
•
pr
1
(
(
𝑎
,
𝑏
)
)
:
≡
𝑎
•
pr
2
(
(
𝑎
,
𝑏
)
)
:
≡
𝑏
Here, our goal is to define
rec
Σ
𝑥
:
𝐴
𝐵
(
𝑥
)
:
Π
(
𝐶
:
𝒰
)
(
Π
(
𝑥
:
𝐴
)
𝐵
(
𝑥
)
→
𝐶
)
→
(
Σ
(
𝑥
:
𝐴
)
𝐵
(
𝑥
)
)
→
𝐶
and its definition is
rec
Σ
𝑥
:
𝐴
𝐵
(
𝑥
)
(
𝐶
,
𝑔
,
(
𝑎
,
𝑏
)
)
:
≡
𝑔
(
pr
1
(
(
𝑎
,
𝑏
)
)
)
(
pr
2
(
(
𝑎
,
𝑏
)
)
)
Let’s verify that the definition concludes with the property we desired once more:
By
𝛽
-reducing on
pr
1
and
pr
2
, we get
rec
Σ
𝑥
:
𝐴
𝐵
(
𝑥
)
(
𝐶
,
𝑔
,
(
𝑎
,
𝑏
)
)
:
≡
𝑔
(
𝑎
)
(
𝑏
)
,
and it correctly Church-encodes the dependent product.
∎
As shown above, the recursor can be defined with the projection functions of (maybe dependent) products.
1.6
#
HoTT 1.6.
Show that if we define
𝐴
×
𝐵
:
≡
∏
𝑥
:
𝟐
𝗋𝖾𝖼
𝟐
(
𝒰
,
𝐴
,
𝐵
,
𝑥
)
, then we can give a definition of
𝗂𝗇𝖽
𝐴
×
𝐵
for
which the definitional equalities stated in §1.5 hold propositionally (i.e. using equality types).
(This requires
the function extensionality axiom, which is introduced in §2.9.)
𝗂𝗇𝖽
𝐴
×
𝐵
:
∏
𝐶
:
𝐴
×
𝐵
→
𝒰
(
(
(
∏
(
𝑥
:
𝐴
)
∏
(
𝑦
:
𝐵
)
𝐶
(
(
𝑥
,
𝑦
)
)
)
)
)
→
∏
𝑥
:
𝐴
×
𝐵
𝐶
(
𝑥
)
𝗂𝗇𝖽
𝐴
×
𝐵
(
𝐶
,
𝑔
,
(
𝑎
,
𝑏
)
)
:
≡
𝑔
(
𝑎
)
(
𝑏
)
(§1.5)
𝖿𝗎𝗇𝖾𝗑𝗍
:
(
∏
𝑥
:
𝐴
(
𝑓
(
𝑥
)
=
𝑔
(
𝑥
)
)
)
→
(
𝑓
=
𝑔
)
(§2.9)
Solution
by
kiwiyou
From definition of
𝐴
×
𝐵
:
≡
∏
𝑥
:
𝟐
𝗋𝖾𝖼
𝟐
(
𝒰
,
𝐴
,
𝐵
,
𝑥
)
, we can natrally try defining our
𝗂𝗇𝖽
𝐴
×
𝐵
:
𝗂𝗇𝖽
′
𝐴
×
𝐵
(
𝐶
,
𝑔
,
𝑥
)
:
≡
𝑔
(
𝑥
(
0
𝟐
)
)
(
𝑥
(
1
𝟐
)
)
Sadly,
𝗂𝗇𝖽
′
𝐴
×
𝐵
has a different type from
𝗂𝗇𝖽
𝐴
×
𝐵
in §1.5:
𝗂𝗇𝖽
′
𝐴
×
𝐵
:
∏
𝐶
:
𝐴
×
𝐵
→
𝒰
(
(
(
∏
(
𝑥
:
𝐴
)
∏
(
𝑦
:
𝐵
)
𝐶
(
(
𝑥
,
𝑦
)
)
)
)
)
→
∏
𝑥
:
𝐴
×
𝐵
𝐶
(
(
𝑥
(
0
𝟐
)
,
𝑥
(
1
𝟐
)
)
)
How can we get value of type
∏
𝑥
:
𝐴
×
𝐵
𝐶
(
𝑥
)
from that of type
∏
𝑥
:
𝐴
×
𝐵
𝐶
(
(
𝑥
(
0
𝟐
)
,
𝑥
(
1
𝟐
)
)
)
?
See this lemma, hidden in §2.3:
Lemma 2.3.1
(Transport)
.
Suppose that
𝑃
is a type family over
𝐴
and that
𝑝
:
𝑥
=
𝐴
𝑦
. Then there is
a function
𝑝
∗
:
𝑃
(
𝑥
)
→
𝑃
(
𝑦
)
.
So if we have
𝑝
:
(
𝑥
(
0
𝟐
)
,
𝑥
(
1
𝟐
)
)
=
𝑥
, we can transport
𝐶
(
(
𝑥
(
0
𝟐
)
,
𝑥
(
1
𝟐
)
)
)
into
𝐶
(
𝑥
)
. Let’s call this
𝑝
as
𝗎𝗇𝗂𝗊
′
𝐴
×
𝐵
.
𝗎𝗇𝗂𝗊
′
𝐴
×
𝐵
:
∏
𝑥
:
𝐴
×
𝐵
(
(
𝑥
(
0
𝟐
)
,
𝑥
(
1
𝟐
)
)
=
𝑥
)
Since we don’t have judgemental equality, it’s time for the function extensionality axiom.
𝗎𝗇𝗂𝗊
′
𝐴
×
𝐵
(
𝑥
)
:
≡
𝖿𝗎𝗇𝖾𝗑𝗍
(
𝗂𝗇𝖽
𝟐
(
𝜆
𝑦
.
(
(
𝑥
(
0
𝟐
)
,
𝑥
(
1
𝟐
)
)
(
𝑦
)
=
𝑥
(
𝑦
)
)
,
𝗋𝖾𝖿𝗅
𝑥
(
0
𝟐
)
,
𝗋𝖾𝖿𝗅
𝑥
(
1
𝟐
)
)
)
Verify the type by case analysis:
(
𝜆
𝑦
.
(
(
𝑥
(
0
𝟐
)
,
𝑥
(
1
𝟐
)
)
(
𝑦
)
=
𝑥
(
𝑦
)
)
(
0
𝟐
)
≡
(
(
𝑥
(
0
𝟐
)
,
𝑥
(
1
𝟐
)
)
(
0
𝟐
)
=
𝑥
(
0
𝟐
)
)
≡
(
(
𝗂𝗇𝖽
𝟐
(
𝗋𝖾𝖼
𝟐
(
𝒰
,
𝐴
,
𝐵
)
,
𝑥
(
0
𝟐
)
,
𝑥
(
1
𝟐
)
)
)
(
0
𝟐
)
=
𝑥
(
0
𝟐
)
)
≡
(
𝑥
(
0
𝟐
)
=
𝑥
(
0
𝟐
)
)
⇒
𝗋𝖾𝖿𝗅
𝑥
(
0
𝟐
)
:
(
𝜆
𝑦
.
(
(
𝑥
(
0
𝟐
)
,
𝑥
(
1
𝟐
)
)
(
𝑦
)
=
𝑥
(
𝑦
)
)
(
0
𝟐
)
(
𝜆
𝑦
.
(
(
𝑥
(
0
𝟐
)
,
𝑥
(
1
𝟐
)
)
(
𝑦
)
=
𝑥
(
𝑦
)
)
(
1
𝟐
)
≡
(
(
𝑥
(
0
𝟐
)
,
𝑥
(
1
𝟐
)
)
(
1
𝟐
)
=
𝑥
(
1
𝟐
)
)
≡
(
(
𝗂𝗇𝖽
𝟐
(
𝗋𝖾𝖼
𝟐
(
𝒰
,
𝐴
,
𝐵
)
,
𝑥
(
0
𝟐
)
,
𝑥
(
1
𝟐
)
)
)
(
1
𝟐
)
=
𝑥
(
1
𝟐
)
)
≡
(
𝑥
(
1
𝟐
)
=
𝑥
(
1
𝟐
)
)
⇒
𝗋𝖾𝖿𝗅
𝑥
(
1
𝟐
)
:
(
𝜆
𝑦
.
(
(
𝑥
(
0
𝟐
)
,
𝑥
(
1
𝟐
)
)
(
𝑦
)
=
𝑥
(
𝑦
)
)
(
1
𝟐
)
Finally, we have
𝗎𝗇𝗂𝗊
′
𝐴
×
𝐵
(
𝑥
)
∗
:
𝐶
(
(
𝑥
(
0
𝟐
)
,
𝑥
(
1
𝟐
)
)
)
→
𝐶
(
𝑥
)
to complete
𝗂𝗇𝖽
′
𝐴
×
𝐵
. This is a new definition:
𝗂𝗇𝖽
′
𝐴
×
𝐵
:
∏
𝐶
:
𝐴
×
𝐵
→
𝒰
(
(
(
∏
(
𝑥
:
𝐴
)
∏
(
𝑦
:
𝐵
)
𝐶
(
(
𝑥
,
𝑦
)
)
)
)
)
→
∏
𝑥
:
𝐴
×
𝐵
𝐶
(
𝑥
)
𝗂𝗇𝖽
′
𝐴
×
𝐵
(
𝐶
,
𝑔
,
𝑥
)
:
≡
𝗎𝗇𝗂𝗊
′
𝐴
×
𝐵
(
𝑥
)
∗
(
𝑔
(
𝑥
(
0
𝟐
)
)
(
𝑥
(
1
𝟐
)
)
)
Remaining question:
𝗂𝗇𝖽
′
𝐴
×
𝐵
=
𝗂𝗇𝖽
𝐴
×
𝐵
holds?
1.8
#
HoTT-1.8.
Define multiplication and exponentiation using
rec
ℕ
. Verify that
(
ℕ
,
+
,
0
,
×
,
1
)
is a semiring
using only
ind
ℕ
. You will probably also need to use symmetry and transitivity of equality, Lemmas 2.1.1
and 2.1.2.
Solution
by
finalchild
Definition of multiplication and exponentiation
Define multiplication and exponentiation as follows. This is just like how we defined add. Note that exponen
tiate has an extra step that reverses the order of parameters.
multiply
:
≡
rec
ℕ
(
ℕ
→
ℕ
,
𝜆
𝑛
.
0
,
𝜆
𝑚
.
𝜆
𝑔
.
𝜆
𝑛
.
𝑛
+
𝑔
(
𝑛
)
)
exponentiate
:
≡
𝜆
𝑚
.
𝜆
𝑛
.
rec
ℕ
(
ℕ
→
ℕ
,
𝜆
𝑚
.
1
,
𝜆
𝑛
.
𝜆
𝑔
.
𝜆
𝑚
.
𝑚
×
𝑔
(
𝑚
)
)
(
𝑛
,
𝑚
)
(
ℕ
,
+
,
0
,
×
,
1
)
is a semiring
Now we verify that
(
ℕ
,
+
,
0
,
×
,
1
)
is a semiring. Note that
summon
(
𝑇
)
is a notation for summoning a known
proof that becomes type
𝑇
with appropriate arguments.
(
ℕ
,
+
,
0
)
is a commutative monoid
Prove
𝑖
+
𝑗
+
𝑘
=
𝑖
+
(
𝑗
+
𝑘
)
with induction.
assoc
+
:
∏
𝑖
,
𝑗
,
𝑘
:
ℕ
𝑖
+
𝑗
+
𝑘
=
𝑖
+
(
𝑗
+
𝑘
)
assoc
+
:
≡
ind
ℕ
(
𝜆
(
𝑖
:
ℕ
)
.
∏
𝑗
,
𝑘
:
ℕ
𝑖
+
𝑗
+
𝑘
=
𝑖
+
(
𝑗
+
𝑘
)
,
assoc
+
,
0
,
assoc
+
,
s
)
assoc
+
,
0
:
∏
𝑗
,
𝑘
:
ℕ
0
+
𝑗
+
𝑘
=
0
+
(
𝑗
+
𝑘
)
assoc
+
,
0
(
𝑗
,
𝑘
)
:
≡
refl
𝑗
+
𝑘
assoc
+
,
s
:
∏
𝑖
:
ℕ
(
∏
𝑗
,
𝑘
:
ℕ
𝑖
+
𝑗
+
𝑘
=
𝑖
+
(
𝑗
+
𝑘
)
)
→
succ
(
𝑖
)
+
𝑗
+
𝑘
=
succ
(
𝑖
)
+
(
𝑗
+
𝑘
)
assoc
+
,
s
(
ℎ
,
𝑖
,
𝑗
,
𝑘
)
:
≡
ap
succ
(
ℎ
(
𝑗
,
𝑘
)
)
Prove that 0 is the identity of
(
ℕ
,
+
)
.
𝜆
𝑖
.
refl
𝑖
:
∏
𝑖
:
ℕ
0
+
𝑖
=
𝑖
ind
ℕ
(
𝜆
(
𝑖
:
ℕ
)
.
𝑖
+
0
=
𝑖
,
refl
0
,
𝜆
𝑖
.
𝜆
ℎ
.
ap
succ
(
ℎ
)
)
:
∏
𝑖
:
ℕ
𝑖
+
0
=
𝑖
Prove
𝑖
+
𝑗
=
𝑗
+
𝑖
with double induction.
commut
+
:
∏
𝑖
,
𝑗
:
ℕ
𝑖
+
𝑗
=
𝑗
+
𝑖
commut
+
:
ind
ℕ
(
𝜆
(
𝑖
:
ℕ
)
.
∏
𝑗
:
ℕ
𝑖
+
𝑗
=
𝑗
+
𝑖
,
commut
+
,
0
,
commut
+
,
s
)
commut
+
,
0
:
∏
𝑗
:
ℕ
0
+
𝑗
=
𝑗
+
0
commut
+
,
0
(
𝑗
)
:
≡
summon
(
𝑗
+
0
=
𝑗
)
)
−
1
commut
+
,
s
:
∏
𝑖
:
ℕ
(
∏
𝑗
:
ℕ
𝑖
+
𝑗
=
𝑗
+
𝑖
)
→
∏
𝑗
:
ℕ
succ
(
𝑖
)
+
𝑗
=
𝑗
+
succ
(
𝑖
)
commut
+
,
s
(
𝑖
,
ℎ
1
)
:
≡
ind
ℕ
(
𝜆
(
𝑗
:
ℕ
)
.
succ
(
𝑖
)
+
𝑗
=
𝑗
+
succ
(
𝑖
)
,
summon
(
succ
(
𝑖
)
+
0
=
succ
(
𝑖
)
)
,
commut_inner
(
𝑖
,
ℎ
1
)
)
commut_inner
:
∏
𝑖
:
ℕ
(
∏
𝑗
:
ℕ
𝑖
+
𝑗
=
𝑗
+
𝑖
)
→
∏
𝑗
:
ℕ
(
succ
(
𝑖
)
+
𝑗
=
𝑗
+
succ
(
𝑖
)
)
→
succ
(
𝑖
)
+
succ
(
𝑗
)
=
succ
(
𝑗
)
+
succ
(
𝑖
)
Prove
commut_inner
(
𝑖
,
ℎ
1
,
𝑗
,
ℎ
2
)
with the composition of three equalities:
succ
(
𝑖
+
succ
(
𝑗
)
)
=
succ
2
(
𝑗
+
𝑖
)
(
by
ℎ
1
)
=
succ
2
(
𝑖
+
𝑗
)
(
by
ℎ
1
)
=
succ
(
𝑗
+
succ
(
𝑖
)
)
(
by
ℎ
2
)
commut_inner
(
𝑖
,
ℎ
1
,
𝑗
,
ℎ
2
)
:
≡
ap
succ
(
ℎ
1
(
succ
(
𝑗
)
)
)
⋅
ap
succ
2
(
ℎ
1
(
𝑗
)
)
−
1
⋅
ap
succ
(
ℎ
2
)
Axioms on ×
Prove that 1 is the identity of
(
ℕ
,
×
)
.
𝜆
𝑖
.
summon
(
𝑖
+
0
=
𝑖
)
:
∏
𝑖
:
ℕ
1
×
𝑖
=
𝑖
ind
ℕ
(
𝜆
(
𝑖
:
ℕ
)
.
𝑖
×
1
=
𝑖
,
refl
0
,
𝜆
𝑖
.
𝜆
ℎ
.
ap
succ
(
ℎ
)
)
:
∏
𝑖
:
ℕ
𝑖
×
1
=
𝑖
Prove 0 annihilates multiplication.
𝜆
𝑖
.
refl
0
:
∏
𝑖
:
ℕ
0
×
𝑖
=
0
ind
ℕ
(
𝜆
(
𝑖
:
ℕ
)
.
𝑖
×
0
=
0
,
refl
0
,
𝜆
𝑖
.
𝜆
ℎ
.
ℎ
)
:
∏
𝑖
:
ℕ
𝑖
×
0
=
0
Prove distribution.
distrbl
:
∏
𝑖
,
𝑗
,
𝑘
:
ℕ
𝑖
×
(
𝑗
+
𝑘
)
=
𝑖
×
𝑗
+
𝑖
×
𝑘
distrbl
:
≡
ind
ℕ
(
𝜆
(
𝑖
:
ℕ
)
.
∏
𝑗
,
𝑘
:
ℕ
𝑖
×
(
𝑗
+
𝑘
)
=
𝑖
×
𝑗
+
𝑖
×
𝑘
,
distrbl
0
,
distrbl
s
)
distrbl
0
:
∏
𝑗
,
𝑘
:
ℕ
0
×
(
𝑗
+
𝑘
)
=
0
×
𝑗
+
0
×
𝑘
distrbl
0
(
𝑗
,
𝑘
)
:
≡
refl
0
distrbl
s
:
∏
𝑖
:
ℕ
(
∏
𝑗
,
𝑘
:
ℕ
𝑖
×
(
𝑗
+
𝑘
)
=
𝑖
×
𝑗
+
𝑖
×
𝑘
)
→
∏
𝑗
,
𝑘
:
ℕ
succ
(
𝑖
)
×
(
𝑗
+
𝑘
)
=
succ
(
𝑖
)
×
𝑗
+
succ
(
𝑖
)
×
𝑘
Prove
distrbl
𝑠
(
𝑖
,
ℎ
,
𝑗
,
𝑘
)
by the composition of equalities:
𝑗
+
𝑘
+
𝑖
×
(
𝑗
+
𝑘
)
=
𝑗
+
𝑘
+
(
𝑖
×
𝑗
+
𝑖
×
𝑘
)
(
by
ℎ
)
=
𝑗
+
(
𝑘
+
𝑖
×
𝑗
+
𝑖
×
𝑘
)
(
by
assoc
+
)
=
𝑗
+
(
𝑖
×
𝑗
+
𝑘
+
𝑖
×
𝑘
)
(
by
commut
+
)
=
𝑗
+
(
𝑖
×
𝑗
+
(
𝑘
+
𝑖
×
𝑘
)
)
(
by
assoc
+
)
=
𝑗
+
𝑖
×
𝑗
+
(
𝑘
+
𝑖
×
𝑘
)
(
by
assoc
+
)
I omit the explicit term for this composition. The components are just
ℎ
,
commut
+
and
assoc
+
wrapped
with ap.
distribr
:
∏
𝑖
,
𝑗
,
𝑘
:
ℕ
(
𝑖
+
𝑗
)
×
𝑘
=
𝑖
×
𝑘
+
𝑗
×
𝑘
distribr
:
≡
ind
ℕ
(
𝜆
(
𝑖
:
ℕ
)
.
∏
𝑗
,
𝑘
:
ℕ
(
𝑖
+
𝑗
)
×
𝑘
=
𝑖
×
𝑘
+
𝑗
×
𝑘
,
distribr
0
,
distribr
s
)
distribr
0
:
∏
𝑗
,
𝑘
:
ℕ
(
0
+
𝑗
)
×
𝑘
=
0
×
𝑘
+
𝑗
×
𝑘
distribr
0
(
𝑗
,
𝑘
)
:
≡
refl
𝑗
×
𝑘
distribr
s
:
∏
𝑖
:
ℕ
(
∏
𝑗
,
𝑘
:
ℕ
(
𝑖
+
𝑗
)
×
𝑘
=
𝑖
×
𝑘
+
𝑗
×
𝑘
)
→
∏
𝑗
,
𝑘
:
ℕ
(
succ
(
𝑖
)
+
𝑗
)
×
𝑘
=
succ
(
𝑖
)
×
𝑘
+
𝑗
×
𝑘
Prove
distribr
𝑠
(
𝑖
,
ℎ
,
𝑗
,
𝑘
)
by the composition of equalities:
𝑘
+
(
𝑖
+
𝑗
)
×
𝑘
=
𝑘
+
(
𝑖
×
𝑘
+
𝑗
×
𝑘
)
(
by
ℎ
)
=
𝑘
+
𝑖
×
𝑘
+
𝑗
×
𝑘
(
by
assoc
+
)
Prove
𝑖
×
𝑗
×
𝑘
=
𝑖
×
(
𝑗
×
𝑘
)
with induction.
assoc
×
:
∏
𝑖
,
𝑗
,
𝑘
:
ℕ
𝑖
×
𝑗
×
𝑘
=
𝑖
×
(
𝑗
×
𝑘
)
assoc
×
:
≡
ind
ℕ
(
𝜆
(
𝑖
:
ℕ
)
.
∏
𝑗
,
𝑘
:
ℕ
𝑖
×
𝑗
×
𝑘
=
𝑖
×
(
𝑗
×
𝑘
)
,
assoc
×
,
0
,
assoc
×
,
s
)
assoc
×
,
0
:
∏
𝑗
,
𝑘
:
ℕ
0
×
𝑗
×
𝑘
=
0
×
(
𝑗
×
𝑘
)
assoc
×
,
0
(
𝑗
,
𝑘
)
:
≡
refl
0
assoc
×
,
s
:
∏
𝑖
:
ℕ
(
∏
𝑗
,
𝑘
:
ℕ
𝑖
×
𝑗
×
𝑘
=
𝑖
×
(
𝑗
×
𝑘
)
)
→
succ
(
𝑖
)
×
𝑗
×
𝑘
=
succ
(
𝑖
)
×
(
𝑗
×
𝑘
)
Prove
assoc
×
,
s
(
𝑖
,
ℎ
)
by the composition of equalities:
(
𝑗
+
𝑖
×
𝑗
)
×
𝑘
=
𝑗
×
𝑘
+
𝑖
×
𝑗
×
𝑘
(
by
distribr
)
=
𝑗
×
𝑘
+
𝑖
×
(
𝑗
×
𝑘
)
(
by
ℎ
)
Therefore,
(
ℕ
,
+
,
0
,
×
,
1
)
is a semiring.
1.10
#
HoTT-1.10.
Show that the Ackermann function
ack
:
ℕ
→
ℕ
→
ℕ
is definable using only
rec
ℕ
satisfying the
following equations:
ack
(
0
,
𝑛
)
≡
succ
(
𝑛
)
ack
(
succ
(
𝑚
)
,
0
)
≡
ack
(
𝑚
,
1
)
ack
(
succ
(
𝑚
)
,
succ
(
𝑛
)
)
≡
ack
(
𝑚
,
ack
(
succ
(
𝑚
)
,
𝑛
)
)
Solution
by
finalchild
ack
:
≡
rec
ℕ
(
ℕ
→
ℕ
,
succ
,
𝜆
(
𝑚
:
ℕ
)
.
𝜆
(
𝑓
:
ℕ
→
ℕ
)
.
rec
ℕ
(
ℕ
,
𝑓
(
1
)
,
𝜆
(
𝑛
:
ℕ
)
.
𝜆
(
𝑐
:
ℕ
)
.
𝑓
(
𝑐
)
)
)
Verify the equations:
ack
(
0
)
≡
succ
ack
(
succ
(
𝑚
)
)
≡
rec
ℕ
(
ℕ
,
ack
(
𝑚
,
1
)
,
𝜆
(
𝑛
:
ℕ
)
.
𝜆
(
𝑐
:
ℕ
)
.
ack
(
𝑚
,
𝑐
)
)
Thus
ack
(
0
,
𝑛
)
≡
succ
(
𝑛
)
ack
(
succ
(
𝑚
)
,
0
)
≡
ack
(
𝑚
,
1
)
ack
(
succ
(
𝑚
)
,
succ
(
𝑛
)
)
≡
(
𝜆
(
𝑛
:
ℕ
)
.
𝜆
(
𝑐
:
ℕ
)
.
ack
(
𝑚
,
𝑐
)
)
(
𝑛
,
ack
(
succ
(
𝑚
)
,
𝑛
)
)
≡
ack
(
𝑚
,
ack
(
succ
(
𝑚
)
,
𝑛
)
)
Note that we folded some instances of recursive calls implicitly.
1.13
#
HoTT 1.13.
Using propositions-as-types, derive the double negation of the principle of excluded middle,
i.e. prove
not (not (P or not P))
.
Solution
by
kiwiyou
We need to find a witness of the type
not (not (P or not P))
.
¬
¬
𝖫𝖤𝖬
:
∏
𝑃
:
𝒰
(
(
𝑃
+
(
𝑃
→
𝟎
)
)
→
𝟎
)
→
𝟎
¬
¬
𝖫𝖤𝖬
:
≡
𝜆
𝑃
.
(
□
:
(
(
𝑃
+
(
𝑃
→
𝟎
)
)
→
𝟎
)
→
𝟎
)
Our first hole must get a function of type
(
𝑃
+
(
𝑃
→
𝟎
)
)
→
𝟎
and derive a contradiction.
¬
¬
𝖫𝖤𝖬
:
≡
𝜆
𝑃
.
𝜆
𝑓
.
(
□
:
𝟎
)
We must use
𝑓
to derive a contradiction as we cannot prove a contradiction directly. Note that
𝑓
derives
a contradiction from a witness of either
𝑃
or
𝑃
→
𝟎
.
𝑃
is not inhabited yet, so we can try constructing a
function of type
𝑃
→
𝟎
.
¬
¬
𝖫𝖤𝖬
:
≡
𝜆
𝑃
.
𝜆
𝑓
.
𝑓
(
𝗂𝗇𝗋
(
□
:
𝑃
→
𝟎
)
)
Our hole now must receive a witness of
𝑃
and derive a contradiction. This time
𝑓
can receive a witness of
𝑃
.
¬
¬
𝖫𝖤𝖬
:
≡
𝜆
𝑃
.
𝜆
𝑓
.
𝑓
(
𝗂𝗇𝗋
(
𝜆
𝑝
.
𝑓
(
𝗂𝗇𝗅
(
𝑝
)
)
)
)
∎
1.15
#
HoTT-1.15.
Show that the indiscernibility of identicals follows from path induction.
Path induction
:
ind
=
𝐴
:
∏
𝐶
:
Π
(
𝑥
,
𝑦
:
𝐴
)
(
𝑥
=
𝐴
𝑦
)
→
𝒰
(
Π
(
𝑥
:
𝐴
)
𝐶
(
𝑥
,
𝑥
,
refl
𝑥
)
)
→
∏
(
𝑥
,
𝑦
:
𝐴
)
∏
(
𝑝
:
𝑥
=
𝐴
𝑦
)
𝐶
(
𝑥
,
𝑦
,
𝑝
)
with equality
ind
=
𝐴
(
𝐶
,
𝑐
,
𝑥
,
𝑥
,
refl
𝑥
)
:
≡
𝑐
(
𝑥
)
Indiscernibility of identicals:
for every family
𝐶
:
𝐴
→
𝒰
there is a function
𝑓
:
∏
(
𝑥
,
𝑦
:
𝐴
)
∏
(
𝑝
:
𝑥
=
𝐴
𝑦
)
𝐶
(
𝑥
)
→
𝐶
(
𝑦
)
such that
𝑓
(
𝑥
,
𝑥
,
refl
𝑥
)
:
≡
id
𝐶
(
𝑥
)
Solution
by
RanolP
Hole Notation (
□
:
𝜏
).
To show the reasoning step, we’ll present a hole notation, which displays the
current goal(s) typed
𝜏
. The hole may be untyped if it’s too obvious or annoying to write explicitly. On
the reasoning step, we’ll replace hole(s) and may introduce new hole(s).
The goal is to construct such
𝑓
. Let’s solve step-by-step.
Given type family
𝐶
:
𝐴
→
𝒰
,
𝑓
:
≡
□
:
∏
(
𝑥
,
𝑦
:
𝐴
)
∏
(
𝑝
:
𝑥
=
𝐴
𝑦
)
𝐶
(
𝑥
)
→
𝐶
(
𝑦
)
≡
ind
=
𝐴
(
□
)
(
□
)
:
∏
(
𝑥
,
𝑦
:
𝐴
)
∏
(
𝑝
:
𝑥
=
𝐴
𝑦
)
𝐶
(
𝑥
)
→
𝐶
(
𝑦
)
≡
ind
=
𝐴
(
𝜆
𝑥
.
𝜆
𝑦
.
𝜆
𝑝
.
𝐶
(
𝑥
)
→
𝐶
(
𝑦
)
)
(
□
:
Π
(
𝑥
:
𝐴
)
𝐶
(
𝑥
)
→
𝐶
(
𝑥
)
)
≡
ind
=
𝐴
(
𝜆
𝑥
.
𝜆
𝑦
.
𝜆
𝑝
.
𝐶
(
𝑥
)
→
𝐶
(
𝑦
)
)
(
𝜆
𝑥
.
(
□
:
𝐶
(
𝑥
)
→
𝐶
(
𝑥
)
)
)
≡
ind
=
𝐴
(
𝜆
𝑥
.
𝜆
𝑦
.
𝜆
𝑝
.
𝐶
(
𝑥
)
→
𝐶
(
𝑦
)
)
(
𝜆
𝑥
.
id
𝐶
(
𝑥
)
)
Let’s verify
𝑓
(
𝑥
,
𝑥
,
refl
𝑥
)
≡
id
𝐶
(
𝑥
)
.
𝑓
(
𝑥
,
𝑥
,
refl
𝑥
)
≡
ind
=
𝐴
(
𝜆
𝑥
.
𝜆
𝑦
.
𝜆
𝑝
.
𝐶
(
𝑥
)
→
𝐶
(
𝑦
)
)
(
𝜆
𝑥
.
id
𝐶
(
𝑥
)
)
(
𝑥
,
𝑥
,
refl
𝑥
)
≡
(
𝜆
𝑥
.
id
𝐶
(
𝑥
)
)
(
𝑥
)
≡
id
𝐶
(
𝑥
)
So, the indicernibility of identicals can be derived from the path induction.
∎