Equivalence of pi and sigma

[JasonGross]

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.

[vladimirias]

It exists in Foundations.
V.

On Feb 20, 2014, at 9:04 PM, Jason Gross notifications@github.com 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.

[mikeshulman]

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?

[JasonGross]

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?

[mikeshulman]

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...

[andrejbauer]

Closing a stale issue.

[mikeshulman]

What does "stale" mean? We haven't yet added this, have we?