(* This is written for the HoTT version of Coq available at https://github.com/HoTT/HoTT *) Require Import Overture. Require Import types.Unit. Theorem prop_unique_unit : forall u : Unit, u = tt. Proof. intro u. induction u. reflexivity. Defined. Theorem prop_unique_product (A B : Type) : forall x : A * B, x = (fst x, snd x). Proof. intro x. induction x. simpl. reflexivity. Defined. Lemma ap {A B : Type} (f : A -> B) : forall x y : A, (x = y) -> (f(x) = f(y)). Proof. intros x y p. induction p. reflexivity. Defined. (* We define our own identity type just for the fun of it *) Inductive eq {A : Type} (x : A) : A -> Type := | refl : eq x x. Notation "x ≈ y" := (eq x y) (at level 70). Theorem inv {A : Type} {x y : A} : (x ≈ y) -> (y ≈ x). Proof. intro p. induction p. exact (refl x). Defined. Notation "p ^-1" := (inv p) (at level 3). Theorem concat {A : Type} {x y z : A} : (x ≈ y) -> (y ≈ z) -> (x ≈ z). Proof. intros p q. induction p. induction q. exact (refl x). Defined. Notation "p ∙ q" := (concat p q) (at level 40). Theorem associate {A : Type} {w x y z : A} (p : w ≈ x) (q : x ≈ y) (r : y ≈ z) : p ∙ (q ∙ r) ≈ (p ∙ q) ∙ r. Proof. induction p. induction q. induction r. simpl. exact (refl (refl w)). Defined. Theorem unit_law {A : Type} {x y : A} : forall p : x ≈ y, (refl x ∙ p ≈ p) * (p ∙ refl y ≈ p). Proof. intro p. induction p. simpl. exact (refl (refl x), refl (refl x)). Defined. Theorem inv_law {A : Type} {x y : A} : forall p : x ≈ y, (p ∙ p ^-1 ≈ refl x) * (p ^-1 ∙ p ≈ refl y). Proof. intro p. induction p. simpl. exact (refl (refl x), refl (refl x)). Defined.