Skip to content

Instantly share code, notes, and snippets.

@JasonGross JasonGross/not_nearly.v

Last active Aug 29, 2015
Embed
What would you like to do?
Composition is not what you think it is! Why "nearly invertible" isn't.
Require Import Overture hit.Interval hit.minus1Trunc types.Bool types.Universe Tactics types.Sigma Equivalences PathGroupoids types.Forall.
Set Implicit Arguments.
Local Open Scope equiv_scope.
Local Open Scope path.
Definition Q `{Univalence} : interval -> Type
:= interval_rectnd
Type Bool Bool
(path_universe negb).
Definition myst `{Univalence} : forall x : interval, Q x.
Proof.
intro x; unfold Q.
eapply (interval_rect Q true (negb true)).
refine (transport_idmap_ap _ _ _ _ _ _ @ (_ @ transport_path_universe negb true)).
refine (ap10 (ap (transport idmap) (interval_rectnd_beta_seg _ _ _ _)) true).
Defined.
Definition i (x : Bool) : interval := if x then zero else one.
Definition id_factored_true `{Univalence} : myst (i true) = true := idpath.
Definition id_factored_false `{Univalence} : myst (i false) = false := idpath.
Definition myst_sig `{Univalence} : interval -> { x : interval & Q x }
:= fun i => (i; myst i).
Definition myst_sig_i `{Univalence} : Bool -> { x : interval & Q x }
:= fun b => myst_sig (i b).
Definition myst_pi_i `{Univalence} : Bool -> { x : Bool & Q (i x) }
:= fun b => (b; myst (i b)).
Definition myst_sig_pi `{Univalence} (x : Bool) : pr2 (myst_sig_i x) = pr2 (myst_pi_i x) := idpath.
Definition transport_myst_eq `{Univalence} : transport Q seg (myst (i true)) = myst (i false)
:= apD myst seg.
Definition myst_sig_eq `{Univalence} : myst_sig (i true) = myst_sig (i false).
Proof.
apply path_sigma_uncurried.
exists seg; apply transport_myst_eq.
Defined.
Definition myst_pi_neq `{Univalence} : ~(myst_pi_i true = myst_pi_i false).
Proof.
intro H'.
apply ((@path_sigma_uncurried _ _ _ _)^-1)%equiv in H'.
destruct H'; simpl in *.
apply (true_ne_false x).
Defined.
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.
Definition compose_dep A B C : (forall x : B, C x) -> forall (f : A -> B), (forall x : A, C (f x))
:= fun f g x => f (g x).
Definition compose_dep_sigma1 `{Funext} {A B C}
: {f : B -> {x : B & C x} & Sect f pr1} ->
forall g : A -> B, {f0 : A -> {x : A & C (g x)} & Sect f0 pr1}
:= fun f g => pi_sigma (@compose_dep A B C (pi_sigma^-1 f) g).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.