Composition is not what you think it is! Why "nearly invertible" isn't.

not_nearly.v

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