Library Containers.Basic_Types

Require Import HoTT.

Definition Empty : Type :=
0 = 1.

Definition Empty_elim (P : Empty → Type) (e : Empty) : P e :=
transport (fun n ⇒ match n with 0 ⇒ P e | _.+1 ⇒ nat end) e^ 0.

Definition Unit :
Type := {n : nat & 0 = n}.

Definition tt :
Unit := (0; idpath).

Definition Unit_elim (P : Unit → Type) (tt_case : P tt) (u : Unit) :
  P u :=
let (n, p) := u in
paths_rect nat 0 (fun n' p' ⇒ P (n'; p')) tt_case n p.

Goal ∀ P tt_case, Unit_elim P tt_case tt = tt_case.
Proof.
  reflexivity.
Defined.

Fixpoint less (n m : nat) {struct m} : Type :=
  match m, n with
    | 0, _ ⇒ Empty
    | m.+1, 0 ⇒ Unit
    | m.+1, n.+1 ⇒ less n m
  end.

Definition Fin (n : nat) : Type :=
{ m : nat & less m n }.

Definition Bool : Type :=
Fin 2.

Definition false : Bool :=
(0; tt).

Definition true : Bool :=
(1; tt).

Definition Bool_elim (P : Bool → Type)
    (false_case : P false) (true_case : P true) (b : Bool) :
  P b.
Proof.
  destruct b as [n l].
  destruct n as [ | [ | n']].
  - apply (Unit_elim (fun u ⇒ P (0; u))).
    exact false_case.
  - apply (Unit_elim (fun u ⇒ P (1; u))).
    exact true_case.
  - apply Empty_elim.
    exact l.
Defined.

Goal ∀ P false_case true_case,
  Bool_elim P false_case true_case false = false_case.
Proof.
  reflexivity.
Qed.

Goal ∀ P false_case true_case,
  Bool_elim P false_case true_case true = true_case.
Proof.
  reflexivity.
Qed.

Definition sum (A B : Type) :=
{ b : Bool & Bool_elim (fun _ ⇒ Type) A B b }.

Definition inl {A B} (a : A) : sum A B :=
(false; a).

Definition inr {A B} (b : B) : sum A B :=
(true; b).

Definition sum_elim {A B} (P : sum A B → Type)
    (inl_case : ∀ a, P (inl a)) (inr_case : ∀ b, P (inr b))
    (s : sum A B) :
  P s.
Proof.
  destruct s as [b x].
  revert x.
  apply (Bool_elim (fun b ⇒ ∀ x, P (b; x))).
  - intros a.
    exact (inl_case a).
  - intros x.
    exact (inr_case x).
Defined.

Goal ∀ A B (P : sum A B → Type) inl_case inr_case a,
  sum_elim P inl_case inr_case (inl a) = inl_case a.
Proof.
  reflexivity.
Qed.

Goal ∀ A B (P : sum A B → Type) inl_case inr_case b,
  sum_elim P inl_case inr_case (inr b) = inr_case b.
Proof.
  reflexivity.
Qed.

Definition merely (A : Type) :=
∀ P : hProp, (A → P) → P.

Definition tr {A} (x : A) : merely A :=
fun P f ⇒ f x.

Definition merely_elim {A} (P : hProp) (f : A → P) :
  merely A → P :=
fun g ⇒ g P f.

Goal ∀ A (P : hProp) f (x : A), merely_elim P f (tr x) = f x.
Proof.
  reflexivity.
Qed.

Goal ∀ `{Funext} A (x y : merely A), x = y.
Proof.
  intros.
  apply path_ishprop.
Qed.