Exercises for Day 1¶
Dependent types¶
Exercise 1.1. (HoTT Book Exercise 1.1)
Given functions f : A → B
and g : B → C
,
define their composite compose A B C f g : A → C
.
Show that composition is associative (definitionally)
and unital (w.r.t. identity
).
Solution for Exercise 1.1
#define compose
( A B C : U)
( f : A → B)
( g : B → C)
: A → C
:= \ x → g (f x)
#define compose-assoc
( A B C D : U)
( f : A → B)
( g : B → C)
( h : C → D)
: compose A B D f (compose B C D g h) = compose A C D (compose A B C f g) h
:= refl
#define compose-left-unit
( A B : U)
( f : A → B)
: compose A B B f (identity B) = f
:= refl
#define compose-right-unit
( A B : U)
( f : A → B)
: compose A A B (identity A) f = f
:= refl
Exercise 1.2. (HoTT Book Exercises 1.2 and 1.3)
Derive recursion and induction principles for products rec-prod A B
using only the projections pr₁
and pr₂
,
and verify that the definitional equalities are valid.
Do the same for Σ-types.
Exercise 1.3. Show that Σ-types are associative in the following sense:
#define concat-assoc
( A : U)
( x y z u : A)
: (p : x = y)
→ (q : y = z)
→ (r : z = u)
→ concat A x y u p (concat A y z u q r)
=_{x = u}
concat A x z u (concat A x y z p q) r
:= ind-path A x (\ w p →
( q : w = z)
→ (r : z = u)
→ concat A x w u p (concat A w z u q r)
=_{x = u}
concat A x z u (concat A x w z p q) r) (\ _ _ → refl) y
#define reassoc-left-Σ
( A : U)
( B : A → U)
( C : (a : A) → B a → U)
: (Σ (a : A), Σ (b : B a), C a b)
→ (Σ (ab : Σ (a : A), B a), C (pr₁ A B ab) (pr₂ A B ab))
:= _exercise
#define reassoc-right-Σ
( A : U)
( B : A → U)
( C : (a : A) → B a → U)
: (Σ (ab : Σ (a : A), B a), C (pr₁ A B ab) (pr₂ A B ab))
→ (Σ (a : A), Σ (b : B a), C a b)
:= _exercise
#define assoc-left-Σ
( A : U)
( B : A → U)
( C : (a : A) → B a → U)
( abc : Σ (a : A), Σ (b : B a), C a b)
: reassoc-right A B C (reassoc-left A B C abc) = abc
:= _exercise
#define assoc-right-Σ
( A : U)
( B : A → U)
( C : (a : A) → B a → U)
( abc : Σ (ab : Σ (a : A), B a), C (pr₁ A B ab) (pr₂ A B ab))
: reassoc-left A B C (reassoc-left A B C abc) = abc
:= _exercise
Propositions as types¶
Exercise 1.4. (HoTT Book Exercise 1.11)
Show that for any type A
, we have ¬ (¬ (¬ A)) → ¬ A
.
Solution for Exercise 1.3
#define exercise-1.3
(A : U)
: ¬ (¬ (¬ A)) → ¬ A
:= \ nnna a → nnna (\ na → na a)
Exercise 1.5. (HoTT Book Exercises 1.12 and 1.13) Using propositions as types interpretation, prove the following tautologies:
- If A, then (if B then A).
- If A, then not (not A).
- If (not A or not B), then not (A and B).
- (*) For any P, double negation of the law of excluded middle holds: not (not (not P or P)).
Identity types¶
Exercise 1.6. (HoTT Book Exercise 1.14) Why do the induction principles for identity types not allow us to construct a the following function?
#define bad
: (x : A)
→ (p : x = x)
→ p = refl_{x}
:= ind-path A x _ refl_{refl_{x}}
Homotopy type theory¶
Exercise 1.7. Formalize both proofs of HoTT Book Lemma 2.1.1. Show that both proofs are equal.
#define path-inv₁
( A : U)
( x y : A)
: (x = y) → (y = x)
:= ind-path' A (\ a b _ → b = a) (\ _ → refl) x y
#define path-inv₂
( A : U)
( x y : A)
: (x = y) → (y = x)
:= ind-path A x (\ w _ → w = x) refl y
#define eq-path-inv₁-path-inv₂
( A : U)
( x y : A)
( p : x = y)
: path-inv₁ A x y p = path-inv₂ A x y p
:= refl
Exercise 1.8. Formalize both proofs of HoTT Book Lemma 2.1.2. Show that both proofs are equal. Consider a third proof and show that it is equal to the other two proofs:
-- a different proof for transitivity
#define concat₃
( A : U)
( x y z : A)
: (x = y) → (y = z) → (x = z)
:= \ p → ind-path A y (\ w _ → x = w) p z
Exercise 1.9. Formalize the proofs of HoTT Book Lemma 2.1.4. Show that different proofs for each point in the lemma are equal.
Solution for Lemma 2.1.4 (i)
#define concat-left-unit
(A : U)
(x y : A)
(p : x = y)
: concat A x x y refl p = p
:= refl
#define concat-right-unit₁
(A : U)
(x y : A)
(p : x = y)
: concat A x y y p refl = p
:= ind-path' A (\ a b p' → concat A a b b p' refl = p') (\ _ → refl) x y p
#define concat-right-unit₂
(A : U)
(x y : A)
(p : x = y)
: concat A x y y p refl = p
:= ind-path A x (\ w p' → concat A x w w p' refl = p') refl y p
#define eq-concat-right-unit₁-concat-right-unit₂
(A : U)
(x y : A)
(p : x = y)
: concat-right-unit₁ A x y p = concat-right-unit₂ A x y p
:= refl
Loop space¶
Consider the definitions of loop space and 2-loop space (HoTT Book Definition 2.1.8):
#define Ω
( A : U)
( a : A)
: U
:= a =_{A} a
#define Ω²
( A : U)
( a : A)
: U
:= Ω (Ω A a) refl_{a}
#define concat-Ω
( A : U)
( a : A)
: Ω A a → Ω A a → Ω A a
:= concat A a a a
Exercise 1.10 (difficult). Formalize the proof of HoTT Book Theorem 2.1.6 (Eckmann-Hilton):
#define Eckmann-Hilton
( A : U)
( a : A)
( α β : Ω A a)
: concat-Ω A a α β = concat-Ω A a β α
:= _exercise