Library MetaCoq.Translations.times_bool_fun2
Set Warnings "-notation-overridden".
From MetaCoq.Template Require Import utils All.
Unset Universe Checking.
From MetaCoq.Translations Require Import translation_utils times_bool_fun MiniHoTT.
Import MCMonadNotation.
Unset MetaCoq Strict Unquote Universe Mode.
MetaCoq Run (TC <- ImplementExisting emptyTC "paths" ;;
TC <- ImplementExisting TC "idpath" ;;
TC <- ImplementExisting TC "paths_ind" ;;
TC <- ImplementExisting TC "transport" ;;
TC <- ImplementExisting TC "sigT" ;;
TC <- ImplementExisting TC "projT1" ;;
TC <- ImplementExisting TC "projT2" ;;
TC <- ImplementExisting TC "existT" ;;
tmDefinition "eqTC" TC).
Next Obligation.
tIntro A. tIntro x. tIntro y. exact (x = y).
Defined.
Next Obligation.
tIntro A. tIntro x. exact 1.
Defined.
Next Obligation.
tIntro A. tIntro a. tIntro P. tIntro t. tIntro y. tIntro p.
exact (paths_ind a (fun y p ⇒ π1 (π1 P y) p) t y p).
Defined.
Next Obligation.
tIntro A. tIntro P. tIntro x. tIntro y. tIntro p. tIntro t.
exact (transport (π1 P) p t).
Defined.
Next Obligation.
tIntro A. tIntro B. exact (sigT (π1 B)).
Defined.
Next Obligation.
tIntro A. tIntro B. tIntro u. exact u.1.
Defined.
Next Obligation.
tIntro A. tIntro B. tIntro u. exact u.2.
Defined.
Next Obligation.
tIntro A. tIntro B. tIntro x. tIntro y. exact (x; y).
Defined.
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).
unshelve econstructor. exact (fun y ⇒ y).
split; intro; exact 1.
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.
repeat unshelve econstructor.
exact (transport idmap p).
exact (transport idmap p^).
all: unfold coe; intro.
exact (transport_Vp idmap _ _).
exact (transport_pV idmap _ _).
Defined.
Definition UA := ∀ A B, isequiv (id2equiv A B).
MetaCoq Run (TC <- Translate eqTC "isequiv" ;;
TC <- Translate TC "equiv" ;;
TC <- ImplementExisting TC "eq" ;;
TC <- Translate TC "inverse" ;;
tmDefinition "eqTC2" TC).
Next Obligation.
tIntro A. tIntro x. tIntro y. exact (@eq A x y).
Defined.
Definition contr A := ∃ x : A, ∀ y, x = y.
Definition weakFunext
:= ∀ (A : Type) (P : A → Type), (∀ x, contr (P x)) → contr (∀ x, P x).
MetaCoq Run (TC <- Translate eqTC2 "contr" ;;
TC <- Translate TC "weakFunext" ;;
tmDefinition "eqTC3" TC).
Goal weakFunextᵗ → False.
intro H. tSpecialize H unit. tSpecialize H (pair (fun _ ⇒ unit) true).
simple refine (let H' := π1 H _ in _).
- tIntro x. lazy. ∃ tt. tIntro y; now destruct y.
- lazy in H'. destruct H' as [H1 H2]; clear H.
tSpecialize H2 (pair (π1 H1) (negb (π2 H1))).
apply (f_equal π2) in H2. lazy in H2.
set (π2 H1) in H2. change (b = negb b) in H2.
destruct b; inversion H2.
Defined.
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.
destruct R as [f [g e]].
∃ (g C.1). intro y.
refine (ap g _ @ e y).
exact (C.2 (f y)).
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α.
intros H A P C.
refine (H (sigT P) A (_; _) _).
unshelve econstructor.
exact (fun x ⇒ (x; (C x).1)).
lazy. econstructor.
intros [x y]. refine (path_sigma' P 1 _). exact ((C x).2 y).
intro; exact 1.
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α.
intros A P H.
simple refine (_; (_; _)).
- intro f. ∃ (fun x ⇒ (x; f x)). exact 1.
- intros [g p] x. refine (_ # (g x).2).
exact (ap10 p x).
- intro f; lazy. exact 1. Defined.
Definition UA_postcomposeequiv' : UA → postcompose_equiv.
intros ua A B e X. repeat unshelve econstructor.
- intros f x. exact (e.2.1 (f x)).
- intro f.
Admitted.
Definition αequiv_weakfunext : contr_isequivα → weakFunext.
intros Hα A P H.
refine (contr_retract _ _).
2: exact (equiv_contrfib _ (Hα A P H) idmap).
exact (contr_retract_α A P H).
Defined.
From MetaCoq.Template Require Import utils All.
Unset Universe Checking.
From MetaCoq.Translations Require Import translation_utils times_bool_fun MiniHoTT.
Import MCMonadNotation.
Unset MetaCoq Strict Unquote Universe Mode.
MetaCoq Run (TC <- ImplementExisting emptyTC "paths" ;;
TC <- ImplementExisting TC "idpath" ;;
TC <- ImplementExisting TC "paths_ind" ;;
TC <- ImplementExisting TC "transport" ;;
TC <- ImplementExisting TC "sigT" ;;
TC <- ImplementExisting TC "projT1" ;;
TC <- ImplementExisting TC "projT2" ;;
TC <- ImplementExisting TC "existT" ;;
tmDefinition "eqTC" TC).
Next Obligation.
tIntro A. tIntro x. tIntro y. exact (x = y).
Defined.
Next Obligation.
tIntro A. tIntro x. exact 1.
Defined.
Next Obligation.
tIntro A. tIntro a. tIntro P. tIntro t. tIntro y. tIntro p.
exact (paths_ind a (fun y p ⇒ π1 (π1 P y) p) t y p).
Defined.
Next Obligation.
tIntro A. tIntro P. tIntro x. tIntro y. tIntro p. tIntro t.
exact (transport (π1 P) p t).
Defined.
Next Obligation.
tIntro A. tIntro B. exact (sigT (π1 B)).
Defined.
Next Obligation.
tIntro A. tIntro B. tIntro u. exact u.1.
Defined.
Next Obligation.
tIntro A. tIntro B. tIntro u. exact u.2.
Defined.
Next Obligation.
tIntro A. tIntro B. tIntro x. tIntro y. exact (x; y).
Defined.
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).
unshelve econstructor. exact (fun y ⇒ y).
split; intro; exact 1.
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.
repeat unshelve econstructor.
exact (transport idmap p).
exact (transport idmap p^).
all: unfold coe; intro.
exact (transport_Vp idmap _ _).
exact (transport_pV idmap _ _).
Defined.
Definition UA := ∀ A B, isequiv (id2equiv A B).
MetaCoq Run (TC <- Translate eqTC "isequiv" ;;
TC <- Translate TC "equiv" ;;
TC <- ImplementExisting TC "eq" ;;
TC <- Translate TC "inverse" ;;
tmDefinition "eqTC2" TC).
Next Obligation.
tIntro A. tIntro x. tIntro y. exact (@eq A x y).
Defined.
Definition contr A := ∃ x : A, ∀ y, x = y.
Definition weakFunext
:= ∀ (A : Type) (P : A → Type), (∀ x, contr (P x)) → contr (∀ x, P x).
MetaCoq Run (TC <- Translate eqTC2 "contr" ;;
TC <- Translate TC "weakFunext" ;;
tmDefinition "eqTC3" TC).
Goal weakFunextᵗ → False.
intro H. tSpecialize H unit. tSpecialize H (pair (fun _ ⇒ unit) true).
simple refine (let H' := π1 H _ in _).
- tIntro x. lazy. ∃ tt. tIntro y; now destruct y.
- lazy in H'. destruct H' as [H1 H2]; clear H.
tSpecialize H2 (pair (π1 H1) (negb (π2 H1))).
apply (f_equal π2) in H2. lazy in H2.
set (π2 H1) in H2. change (b = negb b) in H2.
destruct b; inversion H2.
Defined.
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.
destruct R as [f [g e]].
∃ (g C.1). intro y.
refine (ap g _ @ e y).
exact (C.2 (f y)).
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α.
intros H A P C.
refine (H (sigT P) A (_; _) _).
unshelve econstructor.
exact (fun x ⇒ (x; (C x).1)).
lazy. econstructor.
intros [x y]. refine (path_sigma' P 1 _). exact ((C x).2 y).
intro; exact 1.
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α.
intros A P H.
simple refine (_; (_; _)).
- intro f. ∃ (fun x ⇒ (x; f x)). exact 1.
- intros [g p] x. refine (_ # (g x).2).
exact (ap10 p x).
- intro f; lazy. exact 1. Defined.
Definition UA_postcomposeequiv' : UA → postcompose_equiv.
intros ua A B e X. repeat unshelve econstructor.
- intros f x. exact (e.2.1 (f x)).
- intro f.
Admitted.
Definition αequiv_weakfunext : contr_isequivα → weakFunext.
intros Hα A P H.
refine (contr_retract _ _).
2: exact (equiv_contrfib _ (Hα A P H) idmap).
exact (contr_retract_α A P H).
Defined.