Library MetaCoq.Translations.times_bool_fun2

Definition isequiv {A B} (f : A → B) :=
  ∃ (g : B → A) (H1 : ∀ x, paths (g (f x)) x), (∀ y, paths (f (g y)) y).

Definition idequiv A : @isequiv A A (fun x ⇒ x).
Defined.

Definition equiv A B := ∃ f, @isequiv A B f.

Definition coe {A B} (p : A = B) : A → B
  := transport idmap p.

Definition transport_pV {A : Type} (P : A → Type) {x y : A} (p : x = y)
  : ∀ z : P y, p # p^ # z = z
  := paths_ind x (fun y p ⇒ ∀ z : P y, p # p^ # z = z) (fun z ⇒ 1) y p.

Definition transport_Vp {A : Type} (P : A → Type) {x y : A} (p : x = y)
  : ∀ z : P x, p^ # p # z = z
  := paths_ind x (fun y p ⇒ ∀ z : P x, p^ # p # z = z) (fun z ⇒ 1) y p.

Definition id2equiv A B (p : A = B) : equiv A B.
Defined.

Definition UA := ∀ A B, isequiv (id2equiv A B).


Definition contr A := ∃ x : A, ∀ y, x = y.
Definition weakFunext
  := ∀ (A : Type) (P : A → Type), (∀ x, contr (P x)) → contr (∀ x, P x).


Goal weakFunextᵗ → False.

Definition retract A B := ∃ (f : A → B) (g : B → A), g o f == idmap.

Definition contr_retract {A B} (R : retract A B) (C : contr B) : contr A.
Defined.

Definition postcompose_equiv
  := ∀ A B (e : equiv A B) A', isequiv (fun (g : A' → A) ⇒ e.1 o g).

Definition UA_postcomposeequiv : UA → postcompose_equiv.
Admitted.

Definition α {A} (P : A → Type) := fun (g : A → sigT P) ⇒ pr1 o g.

Definition contr_isequivα := ∀ A P, (∀ x, contr (P x)) → isequiv (@α A P).

Definition postcomposeequiv_αequiv
  : postcompose_equiv → contr_isequivα.
Defined.

Definition fib {A B} (f : A → B) y := ∃ x, f x = y.

Definition equiv_contrfib {A B} (f : A → B) (Hf : isequiv f) y : contr (fib f y).
Admitted.

Definition contr_retractα
  := ∀ A P, (∀ x, contr (P x)) → retract (∀ x : A, P x) (fib (α P) idmap).

Definition contr_retract_α : contr_retractα.
Defined.


Definition UA_postcomposeequiv' : UA → postcompose_equiv.

Admitted.

Definition αequiv_weakfunext : contr_isequivα → weakFunext.
Defined.