Existential Pontification and Generalized Abstract Digressions

## HoTT exercises in Coq (in progress)

I spent some of my plane ride yesterday working on Coq versions of the exercises in The HoTT book. I got as far as 1.6 (yeah, not very far, perhaps I should make a GitHub repo if other folks are interested in contributing skeletons. Don't know what to do about the solutions though). All of these have been test solved.

You will need HoTT/coq in order to run this development; instructions on how to install it are here.

Update. Solutions and more exercises can be found at the HoTT-coqex repository. I’ve done all of the nontrivial homotopy-specific exercises, and left out some of the more standard type theory exercises (which aren’t really homotopy specific). Some of the solutions are really terrible and could use some sprucing up.

```Require Import HoTT.

(* Exercise 1.1 *)
Definition mycompose {A B C : Type} (g : B -> C) (f : A -> B) : A -> C := admit.

Goal forall (A B C D : Type) (f : A -> B) (g : B -> C) (h : C -> D),
mycompose h (mycompose g f) = mycompose (mycompose h g) f.

(* Exercise 1.2 *)
Section ex_1_2_prod.
Variable A B : Type.
Check @fst.
Check @snd.
Definition my_prod_rec (C : Type) (g : A -> B -> C) (p : A * B) : C := admit.
Goal fst = my_prod_rec A (fun a => fun b => a). Admitted.
Goal snd = my_prod_rec B (fun a => fun b => b). Admitted.
End ex_1_2_prod.

Section ex_1_2_sig.
Variable A : Type.
Variable B : A -> Type.
Check @projT1.
Check @projT2.
Definition my_sig_rec (C : Type) (g : forall (x : A), B x -> C) (p : exists (x : A), B x) : C := admit.
Goal @projT1 A B = my_sig_rec A (fun a => fun b => a). Admitted.
(* What goes wrong when you try to prove this for projT2? *)
End ex_1_2_sig.

(* Exercise 1.3 *)

Definition refl {A : Type} (x : A) : x = x := 1%path.

Section ex_1_3_prod.
Variable A B : Type.
(* Given by the book *)
Definition uppt : forall (x : A * B), ((fst x, snd x) = x) :=
fun p => match p with (a,b) => refl (a,b) end.
Definition my_prod_ind (C : A * B -> Type) (g : forall (x : A) (y : B), C (x, y)) (x : A * B) : C x := admit.
Goal forall C g a b, my_prod_ind C g (a, b) = g a b. Admitted.
End ex_1_3_prod.

Section ex_1_3_sig.
Variable A : Type.
Variable B : A -> Type.
Definition sig_uppt : forall (x : exists (a : A), B a), ((projT1 x; projT2 x) = x) := admit.
Definition mysig_ind (C : (exists (a : A), B a) -> Type) (g : forall (a : A) (b : B a), C (a; b)) (x : exists (a : A), B a) : C x := admit.
Goal forall C g a b, mysig_ind C g (a; b) = g a b. Admitted.
End ex_1_3_sig.

(* Exercise 1.4 *)
Fixpoint iter (C : Type) (c0 : C) (cs : C -> C) (n : nat) : C :=
match n with
| 0 => c0
| S n' => cs (iter C c0 cs n')
end.
Definition mynat_rec (C : Type) : C -> (nat -> C -> C) -> nat -> C := admit.
Eval compute in mynat_rec (list nat) nil (@cons nat) 2.
Eval compute in nat_rect (fun _ => list nat) nil (@cons nat) 2.

(* Exercise 1.5 *)
Definition mycoprod (A B : Type) := exists (x : Bool), Bool_rect (fun _ => Type) A B x.

Section ex_1_5.
Variable A B : Type.
Definition inl := existT (Bool_rect (fun _ => Type) A B) true.
Definition inr := existT (Bool_rect (fun _ => Type) A B) false.
Definition mycoprod_ind (C : mycoprod A B -> Type)
(l : forall (a : A), C (inl a))
(r : forall (b : B), C (inr b))
(x : mycoprod A B) : C x := admit.
Goal forall C l r x, mycoprod_ind C l r (inl x) = l x. Admitted.
Goal forall C l r x, mycoprod_ind C l r (inr x) = r x. Admitted.
End ex_1_5.

(* Exercise 1.6 *)

Definition myprod (A B : Type) := forall (x : Bool), Bool_rect (fun _ => Type) A B x.
Section ex_1_6.
Context `{Funext}.
Variable A B : Type.
Definition mypr1 (p : myprod A B) := p true.
Definition mypr2 (p : myprod A B) := p false.
Definition mymkprod (a : A) (b : B) : myprod A B := Bool_rect (Bool_rect (fun _ => Type) A B) a b.
Definition myprod_ind (C : myprod A B -> Type)
(g : forall (x : A) (y : B), C (mymkprod x y)) (x : myprod A B) : C x := admit.
Goal forall C g a b, myprod_ind C g (mymkprod a b) = g a b. Admitted.
End ex_1_6.
```

Actually, I lied. I haven't proved the last goal in exercise 1.6; my trouble is I don't know how to get function extensionality to compute, but I’m sure it’s something simple...

### 5 Responses to “HoTT exercises in Coq (in progress)”

1. Michael Maloney says:

Just in care you’re unaware, funext does not compute. It’s an axiom with no computational rule associated with it. So the job is to avoid writing a program which “gets stuck”.

In order to solve the last problem here, you need to create a lemma that shows that every element of myprod A B is propositionally equal to the pairing of its projections: mymkprod (mypr1 p) (mypr2 p) = p. (This requires extensionality).

Once you have that, your induction rule needs to use it to transport values of the type C(mymkprod (mypr1 p) (mypr2 p)) over to the type C(p). Transport is explained in chapter 2, but first appears under the name “indiscernibility of identicals” earlier in chapter 1.

You end up code that has the form “transport blah (funext blah)”. This is exactly the form of extensionality that tends to break things. Luckily, it doesn’t actually matter here, since you don’t actually need to compute what the transported values are. You just need it to “fix” your types.

Good luck on the exercises! I’m still trying to find time to do them myself…. (Oh nuts…. it’s almost 3am. This is what happens every time I open up Agda………..).

2. Theo says:

Do you know of a good place to learn Coq? I’ve tried once or twice but have never gotten anywhere. I’d like to try these exercises, but I don’t know how to get started.

3. Edward Z. Yang says:

Software Foundations for a gentle introduction (http://www.cis.upenn.edu/~bcpierce/sf/) and CPDT for a less gentle introduction (http://adam.chlipala.net/cpdt/)

4. Edward Z. Yang says:

Michael: Actually, I’ve gotten all the way through what you’ve described; the place I’m stuck is figuring out how to erase the transport when doing the final equality proof.

5. Edward Z. Yang says:

Well, with the help of ##hott we’ve figured it out, and it’s in the solution.