IsEquiv (ap f)

is_equiv_ap.v

Require Import HoTT.

Local Open Scope path_scope.
Local Open Scope equiv_scope.

Section ap.
  Variables A B : Type.
  Variables x y : A.
  Variable f : A -> B.
  Context `{IsEquiv _ _ f}.


  Goal IsEquiv (@ap _ _ f x y).
  Proof.
    apply (isequiv_adjointify
             (ap f)
             (fun H' => (eissect _ _)^ @ ap (f^-1) H' @ eissect _ _));
    hnf;
    [ intro
    | intros [];
      edestruct (eissect f _);
      reflexivity ].
    rewrite !ap_pp.
    rewrite !ap_V.
    rewrite <- !eisadj.
    generalize dependent (f x).
    generalize dependent (f y).
    intros.
    path_induction.
    simpl.
    edestruct (eisretr f _).
    reflexivity.
  Qed.