Require Import VST.msl.base.

Program Definition sig_sig_iff {A: Type} {P Q: A -> Prop}
  (H: forall a, P a <-> Q a) (x: sig P): sig Q := x.
Next Obligation.
(* Goal: Q x *)
  rewrite <- H; auto.
Defined.

Program Definition sig_sig_iff' {A: Type} {P Q: A -> Prop}
  (H: forall a, P a <-> Q a) (x: sig Q): sig P := x.
Next Obligation.
(* Goal: P x *)
  rewrite H; auto.
Defined.

Program Definition sig_sig_eq {A: Type} {P Q: A -> Prop}
  (H: forall a, P a = Q a) (x: sig P): sig Q := x.
Next Obligation.
(* Goal: Q x *)
  rewrite <- H; auto.
Defined.

Program Definition sig_sig_eq' {A: Type} {P Q: A -> Prop}
  (H: forall a, P a = Q a) (x: sig Q): sig P := x.
Next Obligation.
(* Goal: P x *)
  rewrite H; auto.
Defined.

Program Definition sigsig_sig {A: Type} {P Q: A -> Prop}
  (x: sig (fun x: sig P => Q (proj1_sig x))): sig (fun x => P x /\ Q x) := x.

Program Definition sig_sigsig {A: Type} {P Q: A -> Prop}
  (x: sig (fun x => P x /\ Q x)): sig (fun x: sig P => Q (proj1_sig x)) := x.

Program Definition bij_f_sig {A B} (f: bijection A B) (P: A -> Prop)
  (x: sig P): sig (fun b => P (bij_g _ _ f b)) := bij_f _ _ f x.
Next Obligation.
(* Goal: @eq A (bij_g A B f (bij_f A B f x)) x *)
  rewrite bij_gf; auto.
Defined.

Program Definition bij_g_sig {A B} (f: bijection A B) (P: A -> Prop)
  (x: sig (fun b => P (bij_g _ _ f b))): sig P := bij_g _ _ f x.

Lemma sig_sig_iff_iff': forall {A: Type} {P Q: A -> Prop}
  (H: forall a, P a <-> Q a) x,
  (sig_sig_iff H) (sig_sig_iff' H x) = x.
Proof.
(* Goal: forall (A B : Type) (f : bijection A B) (P : forall _ : A, Prop), @eq (forall _ : @sig A P, @sig A P) (@compose (@sig A P) (@sig B (fun b : B => P (bij_g A B f b))) (@sig A P) (@bij_g_sig A B f P) (@bij_f_sig A B f P)) (id (@sig A P)) *)
  intros.
(* Goal: @eq (@sig A P) (@sig_sig_eq' A P Q H (@sig_sig_eq A P Q H x)) x *)
  unfold sig_sig_iff, sig_sig_iff'; simpl.
(* Goal: @eq (@sig A (fun x : A => and (P x) (Q x))) (@exist A (fun x : A => and (P x) (Q x)) (@proj1_sig A (fun x : A => and (P x) (Q x)) x) (@conj (P (@proj1_sig A (fun x : A => and (P x) (Q x)) x)) (Q (@proj1_sig A (fun x : A => and (P x) (Q x)) x)) (sig_sigsig_obligation_1 A P Q x) (sig_sigsig_obligation_2 A P Q x))) x *)
  apply exist_ext'; auto.
Qed.

Lemma sig_sig_iff'_iff: forall {A: Type} {P Q: A -> Prop}
  (H: forall a, P a <-> Q a) x,
  (sig_sig_iff' H) (sig_sig_iff H x) = x.
Proof.
(* Goal: forall (A B : Type) (f : bijection A B) (P : forall _ : A, Prop), @eq (forall _ : @sig A P, @sig A P) (@compose (@sig A P) (@sig B (fun b : B => P (bij_g A B f b))) (@sig A P) (@bij_g_sig A B f P) (@bij_f_sig A B f P)) (id (@sig A P)) *)
  intros.
(* Goal: @eq (@sig A P) (@sig_sig_eq' A P Q H (@sig_sig_eq A P Q H x)) x *)
  unfold sig_sig_iff, sig_sig_iff'; simpl.
(* Goal: @eq (@sig A (fun x : A => and (P x) (Q x))) (@exist A (fun x : A => and (P x) (Q x)) (@proj1_sig A (fun x : A => and (P x) (Q x)) x) (@conj (P (@proj1_sig A (fun x : A => and (P x) (Q x)) x)) (Q (@proj1_sig A (fun x : A => and (P x) (Q x)) x)) (sig_sigsig_obligation_1 A P Q x) (sig_sigsig_obligation_2 A P Q x))) x *)
  apply exist_ext'; auto.
Qed.

Lemma sig_sig_eq_eq': forall {A: Type} {P Q: A -> Prop}
  (H: forall a, P a = Q a) x,
  (sig_sig_eq H) (sig_sig_eq' H x) = x.
Proof.
(* Goal: forall (A B : Type) (f : bijection A B) (P : forall _ : A, Prop), @eq (forall _ : @sig A P, @sig A P) (@compose (@sig A P) (@sig B (fun b : B => P (bij_g A B f b))) (@sig A P) (@bij_g_sig A B f P) (@bij_f_sig A B f P)) (id (@sig A P)) *)
  intros.
(* Goal: @eq (@sig A Q) (@sig_sig_eq A P Q H (@sig_sig_eq' A P Q H x)) x *)
  unfold sig_sig_eq, sig_sig_eq'; simpl.
(* Goal: @eq (@sig A (fun x : A => and (P x) (Q x))) (@exist A (fun x : A => and (P x) (Q x)) (@proj1_sig A (fun x : A => and (P x) (Q x)) x) (@conj (P (@proj1_sig A (fun x : A => and (P x) (Q x)) x)) (Q (@proj1_sig A (fun x : A => and (P x) (Q x)) x)) (sig_sigsig_obligation_1 A P Q x) (sig_sigsig_obligation_2 A P Q x))) x *)
  apply exist_ext'; auto.
Qed.

Lemma sig_sig_eq'_eq: forall {A: Type} {P Q: A -> Prop}
  (H: forall a, P a = Q a) x,
  (sig_sig_eq' H) (sig_sig_eq H x) = x.
Proof.
(* Goal: forall (A B : Type) (f : bijection A B) (P : forall _ : A, Prop), @eq (forall _ : @sig A P, @sig A P) (@compose (@sig A P) (@sig B (fun b : B => P (bij_g A B f b))) (@sig A P) (@bij_g_sig A B f P) (@bij_f_sig A B f P)) (id (@sig A P)) *)
  intros.
(* Goal: @eq (@sig A P) (@sig_sig_eq' A P Q H (@sig_sig_eq A P Q H x)) x *)
  unfold sig_sig_iff, sig_sig_iff'; simpl.
(* Goal: @eq (@sig A (fun x : A => and (P x) (Q x))) (@exist A (fun x : A => and (P x) (Q x)) (@proj1_sig A (fun x : A => and (P x) (Q x)) x) (@conj (P (@proj1_sig A (fun x : A => and (P x) (Q x)) x)) (Q (@proj1_sig A (fun x : A => and (P x) (Q x)) x)) (sig_sigsig_obligation_1 A P Q x) (sig_sigsig_obligation_2 A P Q x))) x *)
  apply exist_ext'; auto.
Qed.

Lemma sig_sigsig_sig: forall {A: Type} {P Q: A -> Prop} x,
  @sig_sigsig A P Q (@sigsig_sig A P Q x) = x.
Proof.
(* Goal: forall (A B : Type) (f : bijection A B) (P : forall _ : A, Prop), @eq (forall _ : @sig A P, @sig A P) (@compose (@sig A P) (@sig B (fun b : B => P (bij_g A B f b))) (@sig A P) (@bij_g_sig A B f P) (@bij_f_sig A B f P)) (id (@sig A P)) *)
  intros.
(* Goal: @eq (@sig A (fun x : A => and (P x) (Q x))) (@sigsig_sig A P Q (@sig_sigsig A P Q x)) x *)
  unfold sig_sigsig, sigsig_sig; simpl.
(* Goal: @eq (@sig (@sig A P) (fun x : @sig A P => Q (@proj1_sig A P x))) (@exist (@sig A P) (fun x : @sig A P => Q (@proj1_sig A P x)) (@exist A P (@proj1_sig A P (@proj1_sig (@sig A P) (fun x : @sig A P => Q (@proj1_sig A P x)) x)) match sigsig_sig_obligation_1 A P Q x with | conj p q => p end) match sigsig_sig_obligation_1 A P Q x with | conj p q => q end) x *)
  destruct x as [[x ?] ?]; simpl.
(* Goal: @eq (@sig (@sig A P) (fun x : @sig A P => Q (@proj1_sig A P x))) (@exist (@sig A P) (fun x : @sig A P => Q (@proj1_sig A P x)) (@exist A P x p) q) (@exist (@sig A P) (fun x : @sig A P => Q (@proj1_sig A P x)) (@exist A P x p) q) *)
  apply exist_ext; auto.
Qed.

Lemma sigsig_sig_sigsig: forall {A: Type} {P Q: A -> Prop} x,
  @sigsig_sig A P Q (@sig_sigsig A P Q x) = x.
Proof.
(* Goal: forall (A B : Type) (f : bijection A B) (P : forall _ : A, Prop), @eq (forall _ : @sig A P, @sig A P) (@compose (@sig A P) (@sig B (fun b : B => P (bij_g A B f b))) (@sig A P) (@bij_g_sig A B f P) (@bij_f_sig A B f P)) (id (@sig A P)) *)
  intros.
(* Goal: @eq (@sig A (fun x : A => and (P x) (Q x))) (@sigsig_sig A P Q (@sig_sigsig A P Q x)) x *)
  unfold sig_sigsig, sigsig_sig; simpl.
(* Goal: @eq (@sig A (fun x : A => and (P x) (Q x))) (@exist A (fun x : A => and (P x) (Q x)) (@proj1_sig A (fun x : A => and (P x) (Q x)) x) (@conj (P (@proj1_sig A (fun x : A => and (P x) (Q x)) x)) (Q (@proj1_sig A (fun x : A => and (P x) (Q x)) x)) (sig_sigsig_obligation_1 A P Q x) (sig_sigsig_obligation_2 A P Q x))) x *)
  apply exist_ext'; auto.
Qed.

Lemma sig_sig_iff_iff'_id: forall {A: Type} {P Q: A -> Prop}
  (H: forall a, P a <-> Q a),
  (sig_sig_iff H) oo (sig_sig_iff' H) = id _.
Proof.
(* Goal: forall (A B : Type) (f : bijection A B) (P : forall _ : A, Prop), @eq (forall _ : @sig A P, @sig A P) (@compose (@sig A P) (@sig B (fun b : B => P (bij_g A B f b))) (@sig A P) (@bij_g_sig A B f P) (@bij_f_sig A B f P)) (id (@sig A P)) *)
  intros.
(* Goal: @eq (forall _ : @sig A (fun x : A => and (P x) (Q x)), @sig A (fun x0 : A => and (P x0) (Q x0))) (@compose (@sig A (fun x : A => and (P x) (Q x))) (@sig (@sig A P) (fun x : @sig A P => Q (@proj1_sig A P x))) (@sig A (fun x : A => and (P x) (Q x))) (@sigsig_sig A P Q) (@sig_sigsig A P Q)) (id (@sig A (fun x : A => and (P x) (Q x)))) *)
  extensionality.
(* Goal: @eq (@sig A P) (@compose (@sig A P) (@sig A Q) (@sig A P) (@sig_sig_eq' A P Q H) (@sig_sig_eq A P Q H) x) (id (@sig A P) x) *)
  unfold id, compose, sig_sig_iff, sig_sig_iff'; simpl.
(* Goal: @eq (@sig A (fun x : A => and (P x) (Q x))) (@exist A (fun x : A => and (P x) (Q x)) (@proj1_sig A (fun x : A => and (P x) (Q x)) x) (@conj (P (@proj1_sig A (fun x : A => and (P x) (Q x)) x)) (Q (@proj1_sig A (fun x : A => and (P x) (Q x)) x)) (sig_sigsig_obligation_1 A P Q x) (sig_sigsig_obligation_2 A P Q x))) x *)
  apply exist_ext'; auto.
Qed.

Lemma bij_fg_sig: forall {A B} (f: bijection A B) (P: A -> Prop) x,
  bij_f_sig f P (bij_g_sig f P x) = x.
Proof.
(* Goal: forall (A B : Type) (f : bijection A B) (P : forall _ : A, Prop), @eq (forall _ : @sig A P, @sig A P) (@compose (@sig A P) (@sig B (fun b : B => P (bij_g A B f b))) (@sig A P) (@bij_g_sig A B f P) (@bij_f_sig A B f P)) (id (@sig A P)) *)
  intros.
(* Goal: @eq (@sig A P) (@bij_g_sig A B f P (@bij_f_sig A B f P x)) x *)
  destruct x; unfold bij_f_sig, bij_g_sig; simpl.
(* Goal: @eq (@sig A P) (@exist A P (bij_g A B f (bij_f A B f x)) (@eq_ind_r A x (fun a : A => P a) p (bij_g A B f (bij_f A B f x)) (bij_gf A B f x))) (@exist A P x p) *)
  apply exist_ext.
(* Goal: @eq B (bij_f A B f (bij_g A B f x)) x *)
  rewrite bij_fg; auto.
Qed.

Lemma bij_gf_sig: forall {A B} (f: bijection A B) (P: A -> Prop) x,
  bij_g_sig f P (bij_f_sig f P x) = x.
Proof.
(* Goal: forall (A B : Type) (f : bijection A B) (P : forall _ : A, Prop), @eq (forall _ : @sig A P, @sig A P) (@compose (@sig A P) (@sig B (fun b : B => P (bij_g A B f b))) (@sig A P) (@bij_g_sig A B f P) (@bij_f_sig A B f P)) (id (@sig A P)) *)
  intros.
(* Goal: @eq (@sig A P) (@bij_g_sig A B f P (@bij_f_sig A B f P x)) x *)
  destruct x; unfold bij_f_sig, bij_g_sig; simpl.
(* Goal: @eq (@sig A P) (@exist A P (bij_g A B f (bij_f A B f x)) (@eq_ind_r A x (fun a : A => P a) p (bij_g A B f (bij_f A B f x)) (bij_gf A B f x))) (@exist A P x p) *)
  apply exist_ext.
(* Goal: @eq A (bij_g A B f (bij_f A B f x)) x *)
  rewrite bij_gf; auto.
Qed.

Lemma sig_sig_iff'_iff_id: forall {A: Type} {P Q: A -> Prop}
  (H: forall a, P a <-> Q a),
  (sig_sig_iff' H) oo (sig_sig_iff H) = id _.
Proof.
(* Goal: forall (A B : Type) (f : bijection A B) (P : forall _ : A, Prop), @eq (forall _ : @sig A P, @sig A P) (@compose (@sig A P) (@sig B (fun b : B => P (bij_g A B f b))) (@sig A P) (@bij_g_sig A B f P) (@bij_f_sig A B f P)) (id (@sig A P)) *)
  intros.
(* Goal: @eq (forall _ : @sig A (fun x : A => and (P x) (Q x)), @sig A (fun x0 : A => and (P x0) (Q x0))) (@compose (@sig A (fun x : A => and (P x) (Q x))) (@sig (@sig A P) (fun x : @sig A P => Q (@proj1_sig A P x))) (@sig A (fun x : A => and (P x) (Q x))) (@sigsig_sig A P Q) (@sig_sigsig A P Q)) (id (@sig A (fun x : A => and (P x) (Q x)))) *)
  extensionality.
(* Goal: @eq (@sig A P) (@compose (@sig A P) (@sig A Q) (@sig A P) (@sig_sig_eq' A P Q H) (@sig_sig_eq A P Q H) x) (id (@sig A P) x) *)
  unfold id, compose, sig_sig_iff, sig_sig_iff'; simpl.
(* Goal: @eq (@sig A (fun x : A => and (P x) (Q x))) (@exist A (fun x : A => and (P x) (Q x)) (@proj1_sig A (fun x : A => and (P x) (Q x)) x) (@conj (P (@proj1_sig A (fun x : A => and (P x) (Q x)) x)) (Q (@proj1_sig A (fun x : A => and (P x) (Q x)) x)) (sig_sigsig_obligation_1 A P Q x) (sig_sigsig_obligation_2 A P Q x))) x *)
  apply exist_ext'; auto.
Qed.

Lemma sig_sig_eq_eq'_id: forall {A: Type} {P Q: A -> Prop}
  (H: forall a, P a = Q a),
  (sig_sig_eq H) oo (sig_sig_eq' H) = id _.
Proof.
(* Goal: forall (A B : Type) (f : bijection A B) (P : forall _ : A, Prop), @eq (forall _ : @sig A P, @sig A P) (@compose (@sig A P) (@sig B (fun b : B => P (bij_g A B f b))) (@sig A P) (@bij_g_sig A B f P) (@bij_f_sig A B f P)) (id (@sig A P)) *)
  intros.
(* Goal: @eq (forall _ : @sig A (fun x : A => and (P x) (Q x)), @sig A (fun x0 : A => and (P x0) (Q x0))) (@compose (@sig A (fun x : A => and (P x) (Q x))) (@sig (@sig A P) (fun x : @sig A P => Q (@proj1_sig A P x))) (@sig A (fun x : A => and (P x) (Q x))) (@sigsig_sig A P Q) (@sig_sigsig A P Q)) (id (@sig A (fun x : A => and (P x) (Q x)))) *)
  extensionality.
(* Goal: @eq (@sig A Q) (@compose (@sig A Q) (@sig A P) (@sig A Q) (@sig_sig_eq A P Q H) (@sig_sig_eq' A P Q H) x) (id (@sig A Q) x) *)
  unfold id, compose, sig_sig_eq, sig_sig_eq'; simpl.
(* Goal: @eq (@sig A (fun x : A => and (P x) (Q x))) (@exist A (fun x : A => and (P x) (Q x)) (@proj1_sig A (fun x : A => and (P x) (Q x)) x) (@conj (P (@proj1_sig A (fun x : A => and (P x) (Q x)) x)) (Q (@proj1_sig A (fun x : A => and (P x) (Q x)) x)) (sig_sigsig_obligation_1 A P Q x) (sig_sigsig_obligation_2 A P Q x))) x *)
  apply exist_ext'; auto.
Qed.

Lemma sig_sig_eq'_eq_id: forall {A: Type} {P Q: A -> Prop}
  (H: forall a, P a = Q a),
  (sig_sig_eq' H) oo (sig_sig_eq H) = id _.
Proof.
(* Goal: forall (A B : Type) (f : bijection A B) (P : forall _ : A, Prop), @eq (forall _ : @sig A P, @sig A P) (@compose (@sig A P) (@sig B (fun b : B => P (bij_g A B f b))) (@sig A P) (@bij_g_sig A B f P) (@bij_f_sig A B f P)) (id (@sig A P)) *)
  intros.
(* Goal: @eq (forall _ : @sig A (fun x : A => and (P x) (Q x)), @sig A (fun x0 : A => and (P x0) (Q x0))) (@compose (@sig A (fun x : A => and (P x) (Q x))) (@sig (@sig A P) (fun x : @sig A P => Q (@proj1_sig A P x))) (@sig A (fun x : A => and (P x) (Q x))) (@sigsig_sig A P Q) (@sig_sigsig A P Q)) (id (@sig A (fun x : A => and (P x) (Q x)))) *)
  extensionality.
(* Goal: @eq (@sig A P) (@compose (@sig A P) (@sig A Q) (@sig A P) (@sig_sig_eq' A P Q H) (@sig_sig_eq A P Q H) x) (id (@sig A P) x) *)
  unfold id, compose, sig_sig_iff, sig_sig_iff'; simpl.
(* Goal: @eq (@sig A (fun x : A => and (P x) (Q x))) (@exist A (fun x : A => and (P x) (Q x)) (@proj1_sig A (fun x : A => and (P x) (Q x)) x) (@conj (P (@proj1_sig A (fun x : A => and (P x) (Q x)) x)) (Q (@proj1_sig A (fun x : A => and (P x) (Q x)) x)) (sig_sigsig_obligation_1 A P Q x) (sig_sigsig_obligation_2 A P Q x))) x *)
  apply exist_ext'; auto.
Qed.

Lemma sig_sigsig_sig_id: forall {A: Type} {P Q: A -> Prop},
  sig_sigsig oo (@sigsig_sig A P Q) = id _.
Proof.
(* Goal: forall (A B : Type) (f : bijection A B) (P : forall _ : A, Prop), @eq (forall _ : @sig A P, @sig A P) (@compose (@sig A P) (@sig B (fun b : B => P (bij_g A B f b))) (@sig A P) (@bij_g_sig A B f P) (@bij_f_sig A B f P)) (id (@sig A P)) *)
  intros.
(* Goal: @eq (forall _ : @sig A (fun x : A => and (P x) (Q x)), @sig A (fun x0 : A => and (P x0) (Q x0))) (@compose (@sig A (fun x : A => and (P x) (Q x))) (@sig (@sig A P) (fun x : @sig A P => Q (@proj1_sig A P x))) (@sig A (fun x : A => and (P x) (Q x))) (@sigsig_sig A P Q) (@sig_sigsig A P Q)) (id (@sig A (fun x : A => and (P x) (Q x)))) *)
  extensionality.
(* Goal: @eq (@sig A (fun x : A => and (P x) (Q x))) (@compose (@sig A (fun x : A => and (P x) (Q x))) (@sig (@sig A P) (fun x : @sig A P => Q (@proj1_sig A P x))) (@sig A (fun x : A => and (P x) (Q x))) (@sigsig_sig A P Q) (@sig_sigsig A P Q) x) (id (@sig A (fun x : A => and (P x) (Q x))) x) *)
  unfold id, compose, sig_sigsig, sigsig_sig; simpl.
(* Goal: @eq (@sig (@sig A P) (fun x : @sig A P => Q (@proj1_sig A P x))) (@exist (@sig A P) (fun x : @sig A P => Q (@proj1_sig A P x)) (@exist A P (@proj1_sig A P (@proj1_sig (@sig A P) (fun x : @sig A P => Q (@proj1_sig A P x)) x)) match sigsig_sig_obligation_1 A P Q x with | conj p q => p end) match sigsig_sig_obligation_1 A P Q x with | conj p q => q end) x *)
  destruct x as [[x ?] ?]; simpl.
(* Goal: @eq (@sig (@sig A P) (fun x : @sig A P => Q (@proj1_sig A P x))) (@exist (@sig A P) (fun x : @sig A P => Q (@proj1_sig A P x)) (@exist A P x p) q) (@exist (@sig A P) (fun x : @sig A P => Q (@proj1_sig A P x)) (@exist A P x p) q) *)
  apply exist_ext; auto.
Qed.

Lemma sigsig_sig_sigsig_id: forall {A: Type} {P Q: A -> Prop},
  sigsig_sig oo (@sig_sigsig A P Q) = id _.
Proof.
(* Goal: forall (A B : Type) (f : bijection A B) (P : forall _ : A, Prop), @eq (forall _ : @sig A P, @sig A P) (@compose (@sig A P) (@sig B (fun b : B => P (bij_g A B f b))) (@sig A P) (@bij_g_sig A B f P) (@bij_f_sig A B f P)) (id (@sig A P)) *)
  intros.
(* Goal: @eq (forall _ : @sig A (fun x : A => and (P x) (Q x)), @sig A (fun x0 : A => and (P x0) (Q x0))) (@compose (@sig A (fun x : A => and (P x) (Q x))) (@sig (@sig A P) (fun x : @sig A P => Q (@proj1_sig A P x))) (@sig A (fun x : A => and (P x) (Q x))) (@sigsig_sig A P Q) (@sig_sigsig A P Q)) (id (@sig A (fun x : A => and (P x) (Q x)))) *)
  extensionality.
(* Goal: @eq (@sig A (fun x : A => and (P x) (Q x))) (@compose (@sig A (fun x : A => and (P x) (Q x))) (@sig (@sig A P) (fun x : @sig A P => Q (@proj1_sig A P x))) (@sig A (fun x : A => and (P x) (Q x))) (@sigsig_sig A P Q) (@sig_sigsig A P Q) x) (id (@sig A (fun x : A => and (P x) (Q x))) x) *)
  unfold id, compose, sig_sigsig, sigsig_sig; simpl.
(* Goal: @eq (@sig A (fun x : A => and (P x) (Q x))) (@exist A (fun x : A => and (P x) (Q x)) (@proj1_sig A (fun x : A => and (P x) (Q x)) x) (@conj (P (@proj1_sig A (fun x : A => and (P x) (Q x)) x)) (Q (@proj1_sig A (fun x : A => and (P x) (Q x)) x)) (sig_sigsig_obligation_1 A P Q x) (sig_sigsig_obligation_2 A P Q x))) x *)
  apply exist_ext'; auto.
Qed.

Lemma bij_fg_sig_id: forall {A B} (f: bijection A B) (P: A -> Prop),
  (bij_f_sig f P) oo (bij_g_sig f P) = id _.
Proof.
(* Goal: forall (A B : Type) (f : bijection A B) (P : forall _ : A, Prop), @eq (forall _ : @sig A P, @sig A P) (@compose (@sig A P) (@sig B (fun b : B => P (bij_g A B f b))) (@sig A P) (@bij_g_sig A B f P) (@bij_f_sig A B f P)) (id (@sig A P)) *)
  intros.
(* Goal: @eq (forall _ : @sig A P, @sig A P) (@compose (@sig A P) (@sig B (fun b : B => P (bij_g A B f b))) (@sig A P) (@bij_g_sig A B f P) (@bij_f_sig A B f P)) (id (@sig A P)) *)
  extensionality x.
(* Goal: @eq (@sig A P) (@compose (@sig A P) (@sig B (fun b : B => P (bij_g A B f b))) (@sig A P) (@bij_g_sig A B f P) (@bij_f_sig A B f P) x) (id (@sig A P) x) *)
  destruct x; unfold compose, id, bij_f_sig, bij_g_sig; simpl.
(* Goal: @eq (@sig A P) (@exist A P (bij_g A B f (bij_f A B f x)) (@eq_ind_r A x (fun a : A => P a) p (bij_g A B f (bij_f A B f x)) (bij_gf A B f x))) (@exist A P x p) *)
  apply exist_ext.
(* Goal: @eq B (bij_f A B f (bij_g A B f x)) x *)
  rewrite bij_fg; auto.
Qed.

Lemma bij_gf_sig_id: forall {A B} (f: bijection A B) (P: A -> Prop),
  (bij_g_sig f P) oo (bij_f_sig f P) = id _.
Proof.
(* Goal: forall (A B : Type) (f : bijection A B) (P : forall _ : A, Prop), @eq (forall _ : @sig A P, @sig A P) (@compose (@sig A P) (@sig B (fun b : B => P (bij_g A B f b))) (@sig A P) (@bij_g_sig A B f P) (@bij_f_sig A B f P)) (id (@sig A P)) *)
  intros.
(* Goal: @eq (forall _ : @sig A P, @sig A P) (@compose (@sig A P) (@sig B (fun b : B => P (bij_g A B f b))) (@sig A P) (@bij_g_sig A B f P) (@bij_f_sig A B f P)) (id (@sig A P)) *)
  extensionality x.
(* Goal: @eq (@sig A P) (@compose (@sig A P) (@sig B (fun b : B => P (bij_g A B f b))) (@sig A P) (@bij_g_sig A B f P) (@bij_f_sig A B f P) x) (id (@sig A P) x) *)
  destruct x; unfold compose, id, bij_f_sig, bij_g_sig; simpl.
(* Goal: @eq (@sig A P) (@exist A P (bij_g A B f (bij_f A B f x)) (@eq_ind_r A x (fun a : A => P a) p (bij_g A B f (bij_f A B f x)) (bij_gf A B f x))) (@exist A P x p) *)
  apply exist_ext.
(* Goal: @eq A (bij_g A B f (bij_f A B f x)) x *)
  rewrite bij_gf; auto.
Qed.

Definition sig_sig_iff_bij {A} {P Q: A -> Prop} (H: forall a, P a <-> Q a):
  bijection (sig P) (sig Q).
  refine (Bijection _ _
           (sig_sig_iff H)
           (sig_sig_iff' H) _ _).
  + apply sig_sig_iff_iff'.
  + apply sig_sig_iff'_iff.
Defined.

Definition sig_sig_eq_bij {A} {P Q: A -> Prop} (H: forall a, P a = Q a):
  bijection (sig P) (sig Q).
  refine (Bijection _ _
           (sig_sig_eq H)
           (sig_sig_eq' H) _ _).
  + apply sig_sig_eq_eq'.
  + apply sig_sig_eq'_eq.
Defined.

Definition sig_sigsig_bij {A} (P Q: A -> Prop):
  bijection (sig (fun a => P a /\ Q a)) (sig (fun a: sig P => Q (proj1_sig a))).
(* Goal: bijection (@sig A (fun a : A => and (P a) (Q a))) (@sig (@sig A P) (fun a : @sig A P => Q (@proj1_sig A P a))) *)
  refine (Bijection _ _ (sig_sigsig) (sigsig_sig) _ _).
  + apply sig_sigsig_sig.
  + apply sigsig_sig_sigsig.
Defined.

Definition bij_sig {A B} (f: bijection A B) (P: A -> Prop):
  bijection (sig P) (sig (fun b => P (bij_g _ _ f b))).
(* Goal: bijection (@sig A P) (@sig B (fun b : B => P (bij_g A B f b))) *)
  refine (Bijection _ _ (bij_f_sig f P) (bij_g_sig f P) _ _).
  + apply bij_fg_sig.
  + apply bij_gf_sig.
Defined.
