Require Import HoTT. Section PathsInProducts. (* Here we prove Theorem 2.6.2 from the book *) Definition pathInProd_to_pairOfPaths {A B} (x y : A * B) : (x = y) -> (fst x = fst y) * (snd x = snd y) := fun pathInProd => (ap fst pathInProd, ap snd pathInProd). Definition pairOfPaths_to_pathInProd {A B} (x y : A * B) : (fst x = fst y) * (snd x = snd y) -> (x = y). induction x as [xA xB]. induction y as [yA yB]. simpl. intro pairOfPaths; destruct pairOfPaths as [pathA pathB]. path_induction. reflexivity. Defined. Lemma homotopy_at_pathInProd {A B} (x y : A * B) : (pairOfPaths_to_pathInProd x y) o (pathInProd_to_pairOfPaths x y) == idmap. Proof. intro pathInProd. unfold compose. path_induction. induction x as [xA xB]. auto. Defined. Lemma homotopy_at_pairOfPaths {A B} (x y : A * B) : (pathInProd_to_pairOfPaths x y) o (pairOfPaths_to_pathInProd x y) == idmap. Proof. intro PairOfPaths; destruct PairOfPaths as [pathA pathB]. induction x as [xA xB]. induction y as [yA yB]. simpl in pathA; simpl in pathB. path_induction. auto. Defined. Theorem PathsInProd_equiv_pairsOfPaths {A B} (x y : A * B) : (x = y) <~> (fst x = fst y) * (snd x = snd y). Proof. exists (pathInProd_to_pairOfPaths x y). (* We need to show that this map is an equivalence. The type of equivalences in the library is the one of half-adjoint equivalences, so we need to use that a map is a half-adjoint equivalence if and only if it is an equivalence in our first definition, which is called 'bi-invertibility' here *) apply equiv_biinv. (* We need two functions from right to left, together with corresponding homotopies, so split into these two cases *) split. (* first case *) exists (pairOfPaths_to_pathInProd x y). exact (homotopy_at_pathInProd x y). (* second case *) exists (pairOfPaths_to_pathInProd x y). exact (homotopy_at_pairOfPaths x y). Defined. End PathsInProducts. Section PathsInUnit. (* Here we prove Theorem 2.8.1 from the book *) Definition pathInUnit_to_Unit (x y : Unit) : (x = y) -> Unit := fun path => tt. Definition Unit_to_pathInUnit (x y : Unit) : Unit -> (x = y). induction x. induction y. intro elemUnit; induction elemUnit. trivial. Defined. Lemma homotopy_at_pathInUnit (x y : Unit) : (Unit_to_pathInUnit x y) o (pathInUnit_to_Unit x y) == idmap. Proof. intro pathInUnit. path_induction. induction x. auto. Defined. Lemma homotopy_at_Unit (x y : Unit) : (pathInUnit_to_Unit x y) o (Unit_to_pathInUnit x y) == idmap. Proof. intro elemUnit. induction elemUnit. auto. Defined. Theorem PathsInUnit_equiv_Unit (x y : Unit) : (x = y) <~> Unit. Proof. (* as above in the case of products *) exists (pathInUnit_to_Unit x y). apply equiv_biinv. split. exists (Unit_to_pathInUnit x y). exact (homotopy_at_pathInUnit x y). exists (Unit_to_pathInUnit x y). exact (homotopy_at_Unit x y). Defined. End PathsInUnit.