Equivalence of pi and sigma · Issue #323 · HoTT/HoTT · GitHub
source link: https://github.com/HoTT/HoTT/issues/323
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
Contributor
JasonGross commented on Feb 21, 2014
Is the following anywhere in the library? Should it go somewhere? (types/Forall? types/Sigma? Misc?)
Require Import Overture Tactics types.Sigma Equivalences PathGroupoids types.Forall. Set Implicit Arguments. Local Open Scope equiv_scope. Section pi_sigma. Context `{Funext} {A} {Q : A -> Type}. Local Notation pi := (forall x, Q x). Local Notation sigma := { f : A -> { x : _ & Q x } & Sect f pr1 }. Let sigma_of_pi : pi -> sigma := (fun f => ((fun x => (x; f x)); (fun x => idpath))). Let pi_of_sigma : sigma -> pi := (fun fh => (fun x => transport Q (fh.2 x) (fh.1 x).2)). Lemma pi_sigma_helper (fh : sigma) x : (x; transport Q (fh.2 x) (fh.1 x).2) = fh.1 x. Proof. generalize (fh.2 x). destruct (fh.1 x); simpl. intro p. apply path_sigma_uncurried. exists (inverse p). simpl. apply transport_Vp. Defined. Lemma pi_sigma_eisretr : Sect pi_of_sigma sigma_of_pi. Proof. intro fh. apply path_sigma_uncurried; simpl. exists (path_forall _ _ (pi_sigma_helper _)). unfold pi_sigma_helper. apply path_forall; intro. unfold Sect. rewrite !transport_forall_constant. transport_path_forall_hammer. destruct fh as [f h]; simpl. generalize (h x). destruct (f x). intro p. destruct p. reflexivity. Qed. Definition pi_sigma : pi <~> sigma. Proof. refine (equiv_adjointify sigma_of_pi pi_of_sigma _ _); [ apply pi_sigma_eisretr | intro; exact idpath ]. Defined. End pi_sigma.
It exists in Foundations.
V.
On Feb 20, 2014, at 9:04 PM, Jason Gross [email protected] wrote:
Is the following anywhere in the library? Should it go somewhere? (types/Forall? types/Sigma? Misc?)
Require Import Overture Tactics types.Sigma Equivalences PathGroupoids types.Forall.
Set Implicit Arguments.
Local Open Scope equiv_scope.Section pi_sigma.
Context `{Funext}
{A}
{Q : A -> Type}.Local Notation pi := (forall x, Q x).
Local Notation sigma := { f : A -> { x : _ & Q x } & Sect f pr1 }.Let sigma_of_pi : pi -> sigma := (fun f => ((fun x => (x; f x)); (fun x => idpath))).
Let pi_of_sigma : sigma -> pi := (fun fh => (fun x => transport Q (fh.2 x) (fh.1 x).2)).Lemma pi_sigma_helper (fh : sigma) x
: (x; transport Q (fh.2 x) (fh.1 x).2) = fh.1 x.
Proof.
generalize (fh.2 x).
destruct (fh.1 x); simpl.
intro p.
apply path_sigma_uncurried.
exists (inverse p).
simpl.
apply transport_Vp.
Defined.Lemma pi_sigma_eisretr : Sect pi_of_sigma sigma_of_pi.
Proof.
intro fh.
apply path_sigma_uncurried; simpl.
exists (path_forall _ _ (pi_sigma_helper _)).
unfold pi_sigma_helper.
apply path_forall; intro.
unfold Sect.
rewrite !transport_forall_constant.
transport_path_forall_hammer.
destruct fh as [f h]; simpl.
generalize (h x).
destruct (f x).
intro p.
destruct p.
reflexivity.
Qed.Definition pi_sigma : pi <~> sigma.
Proof.
refine (equiv_adjointify
sigma_of_pi
pi_of_sigma
_
_);
[ apply pi_sigma_eisretr
| intro; exact idpath ].
Defined.
End pi_sigma.
—
Reply to this email directly or view it on GitHub.
Contributor
mikeshulman commented on Feb 22, 2014
This was in the old version of the library, but I don't see it right now in the new version; maybe it never got ported. We should have it; maybe in types/Sigma? Anyone else have any thoughts?
Here's a proof that I like better, which uses a few other basic lemmas that ought to be added anyway:
Definition equiv_sigma_basecontr {A : Type} (P : A -> Type) `{Contr A}
: sigT P <~> P (center A).
Proof.
refine (@equiv_adjointify (sigT P) (P (center A))
(fun ap => let (a,p):=ap in transport P (contr a)^ p)
(fun p => (center A ; p)) _ _).
intros p. rewrite (path_contr (contr (center A)) (idpath (center A))). exact idpath.
intros [a p]. exact ((path_sigma' P (contr a)^ (idpath (transport P (contr a)^ p)))^).
Defined.
Definition equiv_sigma_comm `(P : A -> Type) `(Q : A -> Type)
: {a : A & {p : P a & Q a}} <~> {a : A & {q : Q a & P a}}.
Proof.
refine (@equiv_adjointify
{a : A & {p : P a & Q a}} {a : A & {q : Q a & P a}}
(fun apq => let (a,pq):=apq in let (p,q):=pq in (a;(q;p)))
(fun aqp => let (a,qp):=aqp in let (q,p):=qp in (a;(p;q)))
_ _).
intros [a [p q]]; apply idpath.
intros [a [q p]]; apply idpath.
Defined.
Instance contr_basedhtpy' `{Funext} `{P : A -> Type} `{f : forall a:A, P a}
: Contr {g : forall x, P x & g == f } | 0.
Proof.
apply (@contr_equiv {g : forall x:A, P x & g = f} {g : forall x:A, P x & g == f}
(equiv_functor_sigma_id (A := forall x:A, P x) (P := fun g => g = f) (Q := fun g => g == f)
(fun g => equiv_inverse (equiv_path_forall g f))));
refine _.
Defined.
Definition pi_sigma `{Funext} {A} {Q : A -> Type}
: (forall x, Q x) <~> { f : A -> { x : _ & Q x } & Sect f pr1 }.
Proof.
refine (equiv_compose' (equiv_functor_sigma'
(P := fun fq => (forall a, pr1 fq a = a))
(Q := fun f => Sect f pr1)
(equiv_sigT_corect (X := A) (fun _ => A) (fun _ => Q)) _) _).
intros [f q]; apply equiv_idmap.
refine (equiv_compose'
(equiv_sigma_assoc (fun f => forall x, Q (f x)) (fun fq => forall a, fq .1 a = a)) _).
refine (equiv_compose'
(equiv_sigma_comm (fun f => forall x, f x = x) (fun f => forall x, Q (f x))) _).
refine (equiv_compose' (equiv_inverse
(equiv_sigma_assoc (fun f:A->A => f == idmap) (fun fq => forall a, Q (fq .1 a)))) _).
exact (equiv_inverse (equiv_sigma_basecontr (fun fq => forall a, Q (fq .1 a)))).
Defined.
My proof of contr_basedhtpy'
requires making contr_equiv
Defined. Why is it currently Qed?
Currently contr_basedhtpy
(with the spots of f and g flipped from the one I needed here) is in FunextVarieties
, but the version there is not generally useful because it uses WeakFunext
rather than Funext
. We should have a version of it somewhere else that uses Funext
. But where? In types/Forall.v
?
Contributor
Author
JasonGross commented on Feb 22, 2014
I feel like you should be able to get typeclass resolution to pick up the equivalence argument to equiv_functor_sigma_id
in contr_basedhtpy'
automatically, if the priorities are set up right. (Also, you mean that your proof of pi_sigma
using contr_basedhtpy'
needs contr_equiv
Defined
, right? I suspect it's Qed
because it's type is contractible.
Can we just prove Funext -> WeakFunext
and set that up as a Hint Immediate
in typeclass resolution?
Contributor
mikeshulman commented on Feb 22, 2014
Oh yes, I misspoke. Having a contractible type isn't a good enough reason to make something Qed, though. Feel free to tweak the proofs...
Closing a stale issue.
Contributor
mikeshulman commented on Oct 13, 2016
What does "stale" mean? We haven't yet added this, have we?
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK