All exercises can be done on paper or in Agda.
Try to do the easy ones (1,2,3,4) if you are new to HoTT or the
medium ones if you are experienced. (The difficult ones are are
only for those who find the medium ones too easy.)

NOTE: If we write something like
f : {a : A} -> B a -> C,
this means that we can keep the argument a : A implicit and don't
have to name it, i.e. if we have a : A and b : B a, we can just
write `f b`.
If we still want to write the argument, we write `f {a} b`.


Exercise 1 (easy)

Recall that we can define transitivity of equality by path induction:
  trans : {a b c : A} -> a = b -> b = c -> a = c
  trans refl q = q
We write `p.q` for `trans p q`.
Prove associativity, i.e. prove
  (p.q).s = p.(q.s)
for all a,b,c,d:A and p:a=b, q:b=c, s:c=d.


Exercise 2 (easy)

Let us define trans2 with the same type as trans by path induction
on the second path, i.e.:
  trans2 : {a b c : A} -> a = b -> b = c -> a = c
  trans2 p refl = p.
Show:
{a b c : A} -> (p : a = b) -> (q : b = c) -> trans p q = trans2 p q


Exercise 3 (easy)

Similarly as above, we have defined symmetry of equality:
  sym : {a b : A} -> a = b -> b = a
  sym refl = refl
Proof that sym is self-inverse, i.e. prove that, for all a,b : A and 
p: a=b, we have:
  sym (sym p) = p.


Exercise 4 (easy)

Recall the construction of `ap`, which applies a function on paths:
For a given function f : A -> B, we define
  ap_f : {a b : A} -> a = b -> f a = f b
  ap_f refl = refl.  
If we have g : B -> C, we write g o f for the composition of the
functions. Show:
  {a b : A} -> (p : a = b) -> ap_(g o f) p = (ap_g o ap_f) p


Exercise 5 (medium)

For a given function f : A -> B, a *pointwise left inverse* is a
function g : B -> A such that (a : A) -> g (f a) = a.

Recall that, again for f : A -> B, the function ap_f is defined as
follows:
  ap_f : {a b : A} -> a = b -> f a = f b
  ap_f refl = refl.

Show: If f has a pointwise left inverse then, for all a,b : A, the
function ap_f {a} {b} has a pointwise left inverse. (Does the other
direction hold as well?)

Remark: The same statement is true with "left" replaced by "right",
but this is more difficult to calculate. You can try to do it as a
difficult exercise. This also implies that, if f is an equivalence,
then ap_f {a} {b} is an equivalence as well. 
See Theorem 2.11.1 in the HoTT book.


Exercise 6 (medium)

"A path between pairs is a pair of paths."
Complete the proof that 
  (a1,b1) = (a2,b2) is equivalent to (a1 = a2) * (b1 = b2).
It is enough to show that they are isomorphic because of Exercise 7.


Exercise 7 (difficult; only recommended if you are already familiar
with HoTT and find all the other exercises easy.)

Given f : A -> B, recall that isIso(f) is the type of triples
  (g, alpha, beta)
with
  g : B -> A
  alpha : (a : A) -> g (f a) = a
  beta  : (b : B) -> f (g b) = b
(note that the HoTT book writes `qinv(f)` for `isIso(f)`.)
Recall that isEqv(f) is the type of quadruples
  (g, alpha, beta, h)
with g, alpha, beta as above and
  h : ap_f (alpha a) = beta (f a).
Construct functions
  isEqv(f) -> isIso(f)   [easy]
and
  isIso(f) -> isEqv(f)   [hard]

Solution: See Theorem 4.2.3 in the HoTT book.


Exercise 8 (difficult; only for experts of HoTT)

In Exercise 7, we have repeated the definition of isIso(f).
There is a canonical function id2iso which turns an equality of types
into an isomorphism of types. What happens if one postulates that the
function id2iso is an equivalence? (Note: The univalence axiom does
the same for the function id2eqv, which turns an equality of types
into an equivalence of types).


Exercise 9 (difficult; a lot of work, has little to do with HoTT)

Show that there are arbitrarily large primes by constructing the term
`bigPrimes` from the "motivating example" of the lecture.