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.
  serapply equiv_adjointify.
  - 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.
  serapply equiv_adjointify.
  - exact (
        fun y x' ⇒
          match x' with
            | None ⇒ snd y
            | Some x ⇒ fst y x
          end).
  - exact (fun y ⇒ (fun x ⇒ y (Some x), y None)).
  - intros y.
    apply apD10^-1; intros [x | ];
      reflexivity.
  - intros y.
    reflexivity.
Qed.