# Library Containers.Equivalences

Require Export HoTT.

Lemma equiv_intensional_choice_finite {B1 B2 C1 C2} :
{b1 : B1 & C1 b1} × {b2 : B2 & C2 b2} <~>
{b : B1 × B2 & C1 (fst b) × C2 (snd b)}.
Proof.
transitivity {_ : {b1 : B1 & C1 b1} & {b2 : B2 & C2 b2}}.
{
symmetry.
apply equiv_sigma_prod0.
}
transitivity {b1 : B1 & {_ : C1 b1 & {b2 : B2 & C2 b2}}}.
{
symmetry.
erapply equiv_sigma_assoc.
}
transitivity {b1 : B1 & {b2 : B2 & {_ : C1 b1 & C2 b2}}}.
{
apply equiv_functor_sigma_id; intros b1.
erapply equiv_sigma_symm.
}
transitivity {b1 : B1 & {b2 : B2 & C1 b1 × C2 b2}}.
{
apply equiv_functor_sigma_id; intros b1.
apply equiv_functor_sigma_id; intros b2.
apply equiv_sigma_prod0.
}
transitivity {b : {_ : B1 & B2} & C1 b.1 × C2 b.2}.
{
erapply equiv_sigma_assoc.
}
serapply equiv_functor_sigma'.
- apply equiv_sigma_prod0.
- intros b. apply reflexivity.
Defined.

Lemma equiv_nat_match `{Funext} (P : nat Type) :
(P 0 × n, P (S n)) <~> ( n, P n).
Proof.
- exact (
fun x n
match n with
| 0 ⇒ fst x
| S n'snd x n'
end
).
- exact (fun x(x 0, x o S)).
- intros x.
by_extensionality n.
destruct n;
reflexivity.
- intros x.
reflexivity.
Defined.

Lemma equiv_shift_sequence_contr_base `{Funext} f :
Contr (f 0) (( n, f n) <~> ( n, f n.+1)).
Proof.
intros ?.
transitivity (f 0 × ( n, f n.+1)). {
symmetry. exact (equiv_nat_match f). }
transitivity (Unit × ( n, f n.+1)). {
apply equiv_functor_prod_r.
apply equiv_contr_unit. }
apply prod_unit_l.
Qed.

Lemma equiv_option_ind `{Funext} {X} (P : option X Type) :
( x, P (Some x)) × P None <~> x', P x'.
Proof.