# Library Containers.Basic_Types

Require Import HoTT.

Definition Empty : Type :=
0 = 1.

Definition Empty_elim (P : Empty Type) (e : Empty) : P e :=
transport (fun nmatch n with 0 ⇒ P e | _.+1nat 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.+1less 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 uP (0; u))).
exact false_case.
- apply (Unit_elim (fun uP (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 ff x.

Definition merely_elim {A} (P : hProp) (f : A P) :
merely A P :=
fun gg 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.