napkin solutions > HoTT
Back to Chapter Selection
Table of Contents
1.2
1.6
1.8
1.10
1.12
1.13
1.15
2.2
2.3
2.6
2.8
2.9
2.14
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.12
#
HoTT-1.12.
Using the propositions as types interpretation, derive the following tautologies.
(i) If
𝐴
, then (if
𝐵
then
𝐴
).
(ii) If
𝐴
, then not (not
𝐴
).
(iii) If (not
𝐴
or not
𝐵
), then not
(
𝐴
and
𝐵
)
.
Solution
by
Jineon Baek (
백진언
) (
xtalclr)
𝖨
:
𝐴
→
(
𝐵
→
𝐴
)
𝖨
:≡
𝜆
(
𝑎
:
𝐴
)
.
(
𝜆
(
𝑏
:
𝐵
)
.
𝑎
)
In words: Assume evidence
𝑎
of
𝐴
. Then assuming the evidence
𝑏
of
𝐵
, the statement
𝐴
is true because
𝑎
is
an evidence of
𝐴
.
𝖨𝖨
:
𝐴
→
(
(
𝐴
→
𝟎
)
→
𝟎
)
𝖨𝖨
:≡
𝜆
(
𝑎
:
𝐴
)
.
(
𝜆
(
𝑛
:
(
𝐴
→
𝟎
)
)
.
𝑛
(
𝑎
)
)
In words: Assume evidence
𝑎
of
𝐴
. Assuming the evidence
𝑛
of not
𝐴
, we get contradiction by evidence
𝑎
of
𝐴
and
𝑛
of not
𝐴
. So it is impossible that not
𝐴
.
𝖨𝖨𝖨
:
(
(
𝐴
→
𝟎
)
+
(
𝐵
→
𝟎
)
)
→
(
𝐴
×
𝐵
)
→
𝟎
𝖨𝖨𝖨
:≡
𝜆
𝑥
.
𝗋𝖾𝖼
(
𝐴
→
𝟎
)
+
(
𝐵
→
𝟎
)
(
(
𝐴
×
𝐵
)
→
𝟎
,
𝖼𝖺𝗌𝖾
𝑎
,
𝖼𝖺𝗌𝖾
𝑏
,
𝑥
)
where
𝖼𝖺𝗌𝖾
𝑎
:
(
𝐴
→
𝟎
)
→
(
𝐴
×
𝐵
)
→
𝟎
𝖼𝖺𝗌𝖾
𝑎
:≡
𝜆
(
𝑐
:
𝐴
→
𝟎
)
.
𝜆
(
𝑝
:
𝐴
×
𝐵
)
.
𝑐
(
𝗉𝗋
1
(
𝑝
)
)
𝖼𝖺𝗌𝖾
𝑏
:
(
𝐵
→
𝟎
)
→
(
𝐴
×
𝐵
)
→
𝟎
𝖼𝖺𝗌𝖾
𝑏
:≡
𝜆
(
𝑐
:
𝐵
→
𝟎
)
.
𝜆
(
𝑝
:
𝐴
×
𝐵
)
.
𝑐
(
𝗉𝗋
2
(
𝑝
)
)
In words: Assume we are given either a evidence of not
𝐴
or a evidence of not
𝐵
.
•
First assume the evidence
𝑐
of not
𝐴
. Then that both
𝐴
and
𝐵
are true is impossible: since the evidence
𝑝
of both
𝐴
and
𝐵
gives the evidence
𝗉𝗋
1
(
𝑝
)
of
𝐴
, we get contradiction by evidence
𝗉𝗋
1
(
𝑝
)
of
𝐴
and
𝑐
of
not
𝐴
.
•
Now assume the evidence
𝑐
of not
𝐵
. Then that both
𝐴
and
𝐵
are true is impossible: since the evidence
𝑝
of both
𝐴
and
𝐵
gives the evidence
𝗉𝗋
2
(
𝑝
)
of
𝐵
, we get contradiction by evidence
𝗉𝗋
2
(
𝑝
)
of
𝐵
and
𝑐
of
not
𝐵
.
So in either case, that both
𝐴
and
𝐵
are true is impossible. So it is not that both
𝐴
and
𝐵
holds.
Solution
by
Jihyeon Kim (
김지현
) (
simnalamburt)
𝖨𝖨𝖨
2
:
(
(
𝐴
→
𝟎
)
+
(
𝐵
→
𝟎
)
)
→
(
𝐴
×
𝐵
)
→
𝟎
𝖨𝖨𝖨
2
(
𝗂𝗇𝗅
(
𝗇𝖺
)
)
:≡
𝜆
𝑝
.
𝗇𝖺
(
𝗉𝗋
1
(
𝑝
)
)
𝖨𝖨𝖨
2
(
𝗂𝗇𝗋
(
𝗇𝖻
)
)
:≡
𝜆
𝑝
.
𝗇𝖻
(
𝗉𝗋
2
(
𝑝
)
)
In words: Assume we are given evidence
𝑥
:
(
¬
𝐴
+
¬
𝐵
)
that either
¬
𝐴
holds or
¬
𝐵
holds.
To show
¬
(
𝐴
×
𝐵
)
, let
𝑝
:
𝐴
×
𝐵
be evidence that both
𝐴
and
𝐵
hold. We proceed by cases on
𝑥
.
•
If
𝑥
is
𝗂𝗇𝗅
(
𝗇𝖺
)
with
𝗇𝖺
:
¬
𝐴
, then from
𝑝
:
𝐴
×
𝐵
we get
𝗉𝗋
1
(
𝑝
)
:
𝐴
. Applying
𝗇𝖺
to
𝗉𝗋
1
(
𝑝
)
yields
0
.
•
If
𝑥
is
𝗂𝗇𝗋
(
𝗇𝖻
)
with
𝗇𝖻
:
¬
𝐵
, then from
𝑝
:
𝐴
×
𝐵
we get
𝗉𝗋
2
(
𝑝
)
:
𝐵
. Applying
𝗇𝖻
to
𝗉𝗋
2
(
𝑝
)
yields
0
.
In either case, assuming
𝐴
×
𝐵
leads to a
0
. Therefore, from
(
¬
𝐴
+
¬
𝐵
)
we conclude
¬
(
𝐴
×
𝐵
)
.
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.
∎
2.2
#
HoTT-2.2.
Show that the three equalities of proofs constructed in the previous exercise form a commutative
triangle. In other words, if the three definitions of concatenation are denoted by
(
𝑝
▪
1
𝑞
)
,
(
𝑝
▪
2
𝑞
)
, and
(
𝑝
▪
3
𝑞
)
, then the concatenated equality
(
𝑝
▪
1
𝑞
)
=
(
𝑝
▪
2
𝑞
)
=
(
𝑝
▪
3
𝑞
)
is equal to the equality
(
𝑝
▪
1
𝑞
)
=
(
𝑝
▪
3
𝑞
)
.
Solution
by
finalchild
𝑒
1
2
𝑥
𝑦
𝑝
𝑧
𝑞
:
(
𝑝
▪
1
𝑞
)
=
(
𝑝
▪
2
𝑞
)
𝑒
2
3
𝑥
𝑦
𝑝
𝑧
𝑞
:
(
𝑝
▪
2
𝑞
)
=
(
𝑝
▪
3
𝑞
)
𝑒
1
3
𝑥
𝑦
𝑝
𝑧
𝑞
:
(
𝑝
▪
1
𝑞
)
=
(
𝑝
▪
3
𝑞
)
Goal: for all
𝑥
,
𝑦
,
𝑝
,
𝑧
,
𝑞
,
(
𝑒
1
2
𝑥
𝑦
𝑝
𝑧
𝑞
)
▪
(
𝑒
2
3
𝑥
𝑦
𝑝
𝑧
𝑞
)
=
𝑒
1
3
𝑥
𝑦
𝑝
𝑧
𝑞
By induction on
𝑝
and
𝑞
, the goal becomes
(
𝑒
1
2
𝑥
𝑥
refl
𝑥
𝑥
refl
𝑥
)
▪
(
𝑒
2
3
𝑥
𝑥
refl
𝑥
𝑥
refl
𝑥
)
=
𝑒
1
3
𝑥
𝑥
refl
𝑥
𝑥
refl
𝑥
which is
refl
refl
𝑥
▪
refl
refl
𝑥
=
refl
refl
𝑥
which is true, judgementally.
2.3
#
HoTT-2.3.
Give a fourth, different, proof of Lemma 2.1.2, and prove that it is equal to the others.
Lemma 2.1.2.
For every type
𝐴
and every
𝑥
,
𝑦
,
𝑧
:
𝐴
, there is a function
(
𝑥
=
𝑦
)
→
(
𝑦
=
𝑧
)
→
(
𝑥
=
𝑧
)
Solution
by
Jihyeon Kim (
김지현
) (
simnalamburt)
𝑥
,
𝑦
,
𝑧
:
𝐴
이고
𝑝
:
𝑥
=
𝑦
,
𝑞
:
𝑦
=
𝑧
라
하자
.
Type family
𝑃
:
𝐴
→
𝒰︀
를
𝑃
(
𝑤
)
≡
(
𝑥
=
𝑤
)
로
정의하면
,
𝑝
:
𝑃
(
𝑦
)
가
된다
.
이제
transport
를
이용한
네
번째
경로
연결
(
concatenation)
을
다음과
같이
정의하자
.
𝑝
⋅
4
𝑞
:
𝑥
=
𝑧
𝑝
⋅
4
𝑞
:
≡
transport
𝑃
(
𝑞
,
𝑝
)
이제
이
정의가
기존의
경로
연결
𝑝
⋅
𝑞
와
같음을
보여야
한다
.
즉
,
다음을
증명해야
한다
.
𝑝
⋅
4
𝑞
=
𝑝
⋅
𝑞
𝑞
에
대한
경로
귀납
(
path induction)
을
사용하자
.
𝑧
를
𝑦
로
,
𝑞
를
refl
𝑦
로
가정하면
충분하다
.
1.
좌변
:
transport
의
정의에
의해
,
경로가
refl
일
때
transport
함수는
항등
함수
(
identity function)
와
정의상
같다
(
definitionally equal).
𝑝
⋅
4
refl
𝑦
≡
transport
𝑃
(
refl
𝑦
,
𝑝
)
≡
𝑝
2.
우변
:
기존
경로
연결의
우측
단위
법칙
(
right unit law)
에
의해
다음이
성립한다
.
𝑝
⋅
refl
𝑦
=
𝑝
따라서
𝑞
≡
refl
𝑦
일
때
𝑝
=
𝑝
가
되어
등식이
성립하므로
,
path induction
에
의해
모든
𝑞
에
대해
𝑝
⋅
4
𝑞
=
𝑝
⋅
𝑞
이다
.
2.6
#
HoTT-2.6.
Prove that if
𝑝
:
𝑥
=
𝑦
, then the function
(
𝑝
▪
–
)
:
(
𝑦
=
𝑧
)
→
(
𝑥
=
𝑧
)
is an equivalence.
Solution
by
finalchild
We have a quasi-inverse given by
(
𝑟
:
𝑥
=
𝑧
)
↦
𝑝
−
1
▪
𝑟
.
We prove the properties needed:
(
(
𝑟
:
𝑥
=
𝑧
)
↦
𝑝
−
1
▪
𝑟
)
∘
(
(
𝑞
:
𝑦
=
𝑧
)
↦
𝑝
▪
𝑞
)
≡
(
(
𝑞
:
𝑦
=
𝑧
)
↦
𝑝
−
1
▪
(
𝑝
▪
𝑞
)
)
∼
id
𝑦
=
𝑧
(
(
𝑞
:
𝑦
=
𝑧
)
↦
𝑝
▪
𝑞
)
∘
(
(
𝑟
:
𝑥
=
𝑧
)
↦
𝑝
−
1
▪
𝑟
)
≡
(
(
𝑟
:
𝑥
=
𝑧
)
↦
𝑝
▪
(
𝑝
−
1
▪
𝑟
)
)
∼
id
𝑥
=
𝑧
2.8
#
HoTT-2.8.
State and prove an analogue of Theorem 2.6.5 for coproducts
Quotation of §2.6
pair
=
:
(
pr
1
(
𝑥
)
=
pr
1
(
𝑦
)
)
×
(
pr
2
(
𝑥
)
=
pr
2
(
𝑦
)
)
→
(
𝑥
=
𝑦
)
⋯
Finally, we consider the functoriality of
ap
under cartesian products. Suppose given types
𝐴
,
𝐵
,
𝐴
′
,
𝐵
′
and functions
𝑔
:
𝐴
→
𝐴
′
and
ℎ
:
𝐵
→
𝐵
′
; then we can define a function
𝑓
:
𝐴
×
𝐵
→
𝐴
′
×
𝐵
′
by
𝑓
(
𝑥
)
:
≡
(
𝑔
(
pr
1
𝑥
)
,
ℎ
(
pr
2
𝑥
)
)
.
Theorem 2.6.5.
In the above situation, given
𝑥
,
𝑦
:
𝐴
×
𝐵
and
𝑝
:
pr
1
𝑥
=
pr
1
𝑦
and
𝑞
:
pr
2
𝑥
=
pr
2
𝑦
,
we have
𝑓
(
pair
=
(
𝑝
,
𝑞
)
)
=
𝑓
(
𝑥
)
=
𝑓
(
𝑦
)
pair
=
(
𝑔
(
𝑝
)
,
ℎ
(
𝑞
)
)
)
Solution
by
RanolP
The core property of the theorem above is followings are same:
•
apply(
𝐴
→
𝐴
′
and
𝐵
→
𝐵
′
) then compose(
𝐴
′
and
𝐵
′
→
𝐴
′
×
𝐵
′
)
•
compose(
𝐴
and
𝐵
→
𝐴
×
𝐵
) then apply(
𝐴
×
𝐵
→
𝐴
′
×
𝐵
′
).
Thus, the analogue for coproducts is followings are same:
•
apply(
𝐴
→
𝐴
′
or
𝐵
→
𝐵
′
) then compose(
𝐴
′
or
𝐵
′
→
𝐴
′
+
𝐵
′
)
•
compose(
𝐴
or
𝐵
→
𝐴
+
𝐵
) then apply(
𝐴
+
𝐵
→
𝐴
′
+
𝐵
′
).
Suppose given types
𝐴
,
𝐵
,
𝐴
′
,
𝐵
′
and functions
𝑔
:
𝐴
→
𝐴
′
and
ℎ
:
𝐵
→
𝐵
′
then we can define a function
𝑓
:
𝐴
+
𝐵
→
𝐴
′
+
𝐵
′
by case analysis:
𝑓
(
inl
(
𝑎
)
)
:
≡
inl
(
𝑔
(
𝑎
)
)
𝑓
(
inr
(
𝑏
)
)
:
≡
inr
(
ℎ
(
𝑏
)
)
In above situation
1.
Given
𝑎
,
𝑎
′
:
𝐴
and
𝑝
:
𝑎
=
𝑎
′
, we have
ap
𝑓
(
ap
inl
(
𝑝
)
)
=
ap
inl
(
ap
𝑔
(
𝑝
)
)
Proof. by path induction on
𝑝
,
ap
𝑓
(
ap
inl
(
refl
𝑎
)
)
=
ap
inl
(
ap
𝑔
(
refl
𝑎
)
)
ap
𝑓
(
refl
inl
(
𝑎
)
)
=
ap
inl
(
refl
𝑔
(
𝑎
)
)
refl
inl
(
𝑔
(
𝑎
)
)
=
refl
inl
(
𝑔
(
𝑎
)
)
2.
Given
𝑏
,
𝑏
′
:
𝐵
and
𝑝
:
𝑏
=
𝑏
′
, we have
ap
𝑓
(
ap
inr
(
𝑝
)
)
=
ap
inr
(
ap
ℎ
(
𝑝
)
)
Proof. by path induction on
𝑝
,
ap
𝑓
(
ap
inr
(
refl
𝑏
)
)
=
ap
inr
(
ap
ℎ
(
refl
𝑏
)
)
ap
𝑓
(
refl
inr
(
𝑏
)
)
=
ap
inr
(
refl
ℎ
(
𝑏
)
)
refl
inr
(
ℎ
(
𝑏
)
)
=
refl
inr
(
ℎ
(
𝑏
)
)
2.9
#
HoTT-2.9.
Prove that coproducts have the expected universal property,
(
𝐴
+
𝐵
→
𝑋
)
≃
(
𝐴
→
𝑋
)
×
(
𝐵
→
𝑋
)
.
Can you generalize this to an equivalence involving dependent functions?
Solution
by
Jihyeon Kim (
김지현
) (
simnalamburt)
먼저
비의존
함수
(
non-dependent function)
버전을
증명하자
.
두
함수
split
(forward,
→
)
와
join
(backward,
←
)
을
다음과
같이
정의한다
.
split
:
(
𝐴
+
𝐵
→
𝑋
)
→
(
𝐴
→
𝑋
)
×
(
𝐵
→
𝑋
)
split
(
ℎ
)
:
≡
(
ℎ
∘
inl
,
ℎ
∘
inr
)
join
:
(
𝐴
→
𝑋
)
×
(
𝐵
→
𝑋
)
→
(
𝐴
+
𝐵
→
𝑋
)
join
(
(
𝑔
,
ℎ
)
)
:
≡
rec
𝐴
+
𝐵
(
𝑋
,
𝑔
,
ℎ
)
이제
두
함수가
서로
역함수
(
inverse)
임을
보이자
.
1.
split
∘
join
∼
id
:
임의의
𝑥
에
대하여
,
by induction on
𝑥
,
(
𝑔
,
ℎ
)
≡
𝑥
split
(
join
(
(
𝑔
,
ℎ
)
)
)
≡
(
join
(
(
𝑔
,
ℎ
)
)
∘
inl
,
join
(
(
𝑔
,
ℎ
)
)
∘
inr
)
≡
(
𝜆
𝑎
.
𝑔
(
𝑎
)
,
𝜆
𝑏
.
ℎ
(
𝑏
)
)
≡
(
𝑔
,
ℎ
)
(
by
η-
conversion
)
So,
split
(
join
(
(
𝑔
,
ℎ
)
)
)
=
(
𝑔
,
ℎ
)
.
2.
join
∘
split
∼
id
:
임의의
𝑓
:
𝐴
+
𝐵
→
𝑋
에
대하여
,
모든
𝑥
:
𝐴
+
𝐵
에서
join
(
split
(
𝑓
)
)
(
𝑥
)
=
𝑓
(
𝑥
)
임을
𝑥
에
대한
귀납법으로
보인다
.
•
𝑥
≡
inl
(
𝑎
)
일
때
:
join
(
split
(
𝑓
)
)
(
inl
(
𝑎
)
)
≡
(
𝑓
∘
inl
)
(
𝑎
)
≡
𝑓
(
inl
(
𝑎
)
)
•
𝑥
≡
inr
(
𝑏
)
일
때
:
join
(
split
(
𝑓
)
)
(
inr
(
𝑏
)
)
≡
(
𝑓
∘
inr
)
(
𝑏
)
≡
𝑓
(
inr
(
𝑏
)
)
점별로
(
pointwise)
같으므로
,
함수
외연성
(
function extensionality)
에
의해
join
(
split
(
𝑓
)
)
=
𝑓
이다
.
다음으로
,
이를
의존
함수
(
dependent function)
버전으로
일반화하자
.
임의의
Type family
𝑃
:
𝐴
+
𝐵
→
𝒰︀
에
대하여
다음이
성립한다
.
(
Π
𝑥
:
𝐴
+
𝐵
𝑃
(
𝑥
)
)
≃
(
Π
𝑎
:
𝐴
𝑃
(
inl
(
𝑎
)
)
)
×
(
Π
𝑏
:
𝐵
𝑃
(
inr
(
𝑏
)
)
)
증명
구조는
위와
완전히
동일하다
.
split
Π
(
ℎ
)
:
≡
(
𝜆
𝑎
.
ℎ
(
inl
(
𝑎
)
)
,
𝜆
𝑏
.
ℎ
(
inr
(
𝑏
)
)
)
join
Π
(
𝑔
,
ℎ
)
:
≡
ind
𝐴
+
𝐵
(
𝜆
𝑥
.
𝑋
,
𝑔
,
ℎ
)
1.
split
Π
(
join
Π
(
𝑔
,
ℎ
)
)
는
정의에
따라
(
𝑔
,
ℎ
)
로
계산된다
(
definitionally equal).
2.
join
Π
(
split
Π
(
𝑓
)
)
는
𝑥
가
inl
(
𝑎
)
일
때와
inr
(
𝑏
)
일
때
모두
𝑓
(
𝑥
)
와
같으므로
,
함수
외연성에
의해
𝑓
와
같다
.
2.14
#
HoTT 2.14.
Suppose we add to type theory the
equality reflection rule
which says that if there is an element
𝑝
:
𝑥
=
𝑦
, then in fact
𝑥
≡
𝑦
. Prove that for any
𝑝
:
𝑥
=
𝑥
, we have
𝑝
≡
𝗋𝖾𝖿𝗅
𝑥
. (This implies that every type
is a set in the sense to be introduced in §3.1; see §7.2.)
Solution
by
kiwiyou
We can have this strange claim under equality reflection rule:
𝗌𝗍𝗋𝖺𝗇𝗀𝖾
:
∏
𝑥
,
𝑦
:
𝐴
∏
𝑞
:
𝑥
=
𝑦
𝑞
=
𝑥
=
𝑦
𝗋𝖾𝖿𝗅
𝑥
Then we can prove this with path induction. We can inhabit
𝗌𝗍𝗋𝖺𝗇𝗀𝖾
:
𝗌𝗍𝗋𝖺𝗇𝗀𝖾
(
𝑥
,
𝑥
,
𝗋𝖾𝖿𝗅
𝑥
)
≡
𝗋𝖾𝖿𝗅
𝗋𝖾𝖿𝗅
𝑥
𝗌𝗍𝗋𝖺𝗇𝗀𝖾
:
≡
𝗂𝗇𝖽
=
𝐴
(
𝜆
𝑥
,
𝑦
:
𝐴
.
𝜆
𝑞
:
𝑥
=
𝑦
.
𝑞
=
𝑥
=
𝑦
𝗋𝖾𝖿𝗅
𝑥
,
𝜆
𝑥
:
𝐴
.
𝗋𝖾𝖿𝗅
𝗋𝖾𝖿𝗅
𝑥
)
So finally, given
𝑝
:
𝑥
=
𝑥
, we have
𝗌𝗍𝗋𝖺𝗇𝗀𝖾
(
𝑥
,
𝑥
,
𝑝
)
:
𝑝
=
𝗋𝖾𝖿𝗅
𝑥
, which is also, by equality reflection rule:
𝑝
≡
𝗋𝖾𝖿𝗅
𝑥
∎