Set Universe Polymorphism.

(* Equivalences *)
Class IsEquiv {A : Type} {B : Type} (f : A -> B) := BuildIsEquiv {
  e_inv : B -> A ;
  e_sect : forall x, e_inv (f x) = x;
  e_retr : forall y, f (e_inv y) = y;
  e_adj : forall x : A, e_retr (f x) = ap f (e_sect x);
}.

(** A class that includes all the data of an adjoint equivalence. *)
Class Equiv A B := BuildEquiv {
  e_fun : A -> B ;
  e_isequiv :> IsEquiv e_fun
}.

 Definition is_adjoint' {A B : Type} (f : A -> B) (g : B -> A)
           (issect : g∘ f == id) (isretr : f  ∘ g == id) (a : A) :
  isretr (f a) = ap f (issect' f g issect isretr a). 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
isretr (f a) = ap f (issect' f g issect isretr a)
 Proof. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
isretr (f a) = ap f (issect' f g issect isretr a)
   unfold issect'. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
isretr (f a) =
ap f
  ((ap g (ap f (issect a)^) @ ap g (isretr (f a))) @
   issect a)
   apply moveL_M1. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
eq_refl =
ap f
  ((ap g (ap f (issect a)^) @ ap g (isretr (f a))) @
   issect a) @ (isretr (f a))^
   repeat rewrite ap_pp. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
eq_refl =
((ap f (ap g (ap f (issect a)^)) @
  ap f (ap g (isretr (f a)))) @
 ap f (issect a)) @ (isretr (f a))^  rewrite <- concat_p_pp; rewrite <- ap_compose. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
eq_refl =
(ap (fun x : B => f (g x)) (ap f (issect a)^) @
 ap f (ap g (isretr (f a)))) @
(ap f (issect a) @ (isretr (f a))^)
   pose  (concat_pA1 (fun b => (isretr b)^) (ap f (issect a))). 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (ap f (issect a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (ap f (issect a)) =
ap f (issect a) @ (fun b : B => (isretr b)^) (f a)
eq_refl =
(ap (fun x : B => f (g x)) (ap f (issect a)^) @
 ap f (ap g (isretr (f a)))) @
(ap f (issect a) @ (isretr (f a))^)
   eapply concat. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (ap f (issect a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (ap f (issect a)) =
ap f (issect a) @ (fun b : B => (isretr b)^) (f a)
eq_refl = ?y  2: { 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (ap f (issect a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (ap f (issect a)) =
ap f (issect a) @ (fun b : B => (isretr b)^) (f a)
?y =
(ap (fun x : B => f (g x)) (ap f (issect a)^) @
 ap f (ap g (isretr (f a)))) @
(ap f (issect a) @ (isretr (f a))^)  apply ap2. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (ap f (issect a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (ap f (issect a)) =
ap f (issect a) @ (fun b : B => (isretr b)^) (f a)
?x =
ap (fun x : B => f (g x)) (ap f (issect a)^) @
ap f (ap g (isretr (f a)))  reflexivity. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (ap f (issect a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (ap f (issect a)) =
ap f (issect a) @ (fun b : B => (isretr b)^) (f a)
?x' = ap f (issect a) @ (isretr (f a))^ exact e.  } 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (ap f (issect a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (ap f (issect a)) =
ap f (issect a) @ (fun b : B => (isretr b)^) (f a)
eq_refl =
(ap (fun x : B => f (g x)) (ap f (issect a)^) @
 ap f (ap g (isretr (f a)))) @
((fun b : B => (isretr b)^) (f (g (f a))) @
 ap (fun b : B => f (g b)) (ap f (issect a)))
   cbn. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (ap f (issect a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (ap f (issect a)) =
ap f (issect a) @ (fun b : B => (isretr b)^) (f a)
eq_refl =
(ap (fun x : B => f (g x)) (ap f (issect a)^) @
 ap f (ap g (isretr (f a)))) @
((isretr (f (g (f a))))^ @
 ap (fun b : B => f (g b)) (ap f (issect a)))  clear e. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
eq_refl =
(ap (fun x : B => f (g x)) (ap f (issect a)^) @
 ap f (ap g (isretr (f a)))) @
((isretr (f (g (f a))))^ @
 ap (fun b : B => f (g b)) (ap f (issect a)))
   pose (concat_pA1 (fun b => (isretr b)^) (isretr (f a))). 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
eq_refl =
(ap (fun x : B => f (g x)) (ap f (issect a)^) @
 ap f (ap g (isretr (f a)))) @
((isretr (f (g (f a))))^ @
 ap (fun b : B => f (g b)) (ap f (issect a)))
   rewrite <- concat_p_pp. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
eq_refl =
ap (fun x : B => f (g x)) (ap f (issect a)^) @
(ap f (ap g (isretr (f a))) @
 ((isretr (f (g (f a))))^ @
  ap (fun b : B => f (g b)) (ap f (issect a))))
   pose (concat_A1p (fun b => (isretr b)) (isretr (f a))). 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0:= concat_A1p (fun b : B => isretr b) (isretr (f a)): ap (fun x : B => f (g x)) (isretr (f a)) @
(fun b : B => isretr b) (f a) =
(fun b : B => isretr b) (f (g (f a))) @
isretr (f a)
eq_refl =
ap (fun x : B => f (g x)) (ap f (issect a)^) @
(ap f (ap g (isretr (f a))) @
 ((isretr (f (g (f a))))^ @
  ap (fun b : B => f (g b)) (ap f (issect a))))
   apply moveL_Vp in e0. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap (fun x : B => f (g x)) (isretr (f a)) =
(isretr (f (g (f a))) @ isretr (f a)) @
(isretr (f a))^
eq_refl =
ap (fun x : B => f (g x)) (ap f (issect a)^) @
(ap f (ap g (isretr (f a))) @
 ((isretr (f (g (f a))))^ @
  ap (fun b : B => f (g b)) (ap f (issect a))))
   rewrite <- concat_p_pp in e0. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap (fun x : B => f (g x)) (isretr (f a)) =
isretr (f (g (f a))) @
(isretr (f a) @ (isretr (f a))^)
eq_refl =
ap (fun x : B => f (g x)) (ap f (issect a)^) @
(ap f (ap g (isretr (f a))) @
 ((isretr (f (g (f a))))^ @
  ap (fun b : B => f (g b)) (ap f (issect a))))  rewrite inv_inv' in e0. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap (fun x : B => f (g x)) (isretr (f a)) =
isretr (f (g (f a))) @ eq_refl
eq_refl =
ap (fun x : B => f (g x)) (ap f (issect a)^) @
(ap f (ap g (isretr (f a))) @
 ((isretr (f (g (f a))))^ @
  ap (fun b : B => f (g b)) (ap f (issect a))))
   rewrite concat_refl in e0. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap (fun x : B => f (g x)) (isretr (f a)) =
isretr (f (g (f a)))
eq_refl =
ap (fun x : B => f (g x)) (ap f (issect a)^) @
(ap f (ap g (isretr (f a))) @
 ((isretr (f (g (f a))))^ @
  ap (fun b : B => f (g b)) (ap f (issect a))))
   rewrite ap_compose in e0. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
eq_refl =
ap (fun x : B => f (g x)) (ap f (issect a)^) @
(ap f (ap g (isretr (f a))) @
 ((isretr (f (g (f a))))^ @
  ap (fun b : B => f (g b)) (ap f (issect a))))
   eapply concat. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
eq_refl = ?y
   2: { 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?y =
ap (fun x : B => f (g x)) (ap f (issect a)^) @
(ap f (ap g (isretr (f a))) @
 ((isretr (f (g (f a))))^ @
  ap (fun b : B => f (g b)) (ap f (issect a))))  apply ap2. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x = ap (fun x : B => f (g x)) (ap f (issect a)^)  reflexivity. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x' =
ap f (ap g (isretr (f a))) @
((isretr (f (g (f a))))^ @
 ap (fun b : B => f (g b)) (ap f (issect a)))  rewrite concat_p_pp. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x' =
(ap f (ap g (isretr (f a))) @ (isretr (f (g (f a))))^) @
ap (fun b : B => f (g b)) (ap f (issect a))  eapply concat. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x' = ?y
        2: { 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?y =
(ap f (ap g (isretr (f a))) @ (isretr (f (g (f a))))^) @
ap (fun b : B => f (g b)) (ap f (issect a))  apply ap2. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x =
ap f (ap g (isretr (f a))) @ (isretr (f (g (f a))))^  eapply concat. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x = ?y
             2:{ 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?y =
ap f (ap g (isretr (f a))) @ (isretr (f (g (f a))))^  apply ap2. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x0 = ap f (ap g (isretr (f a)))  symmetry. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
ap f (ap g (isretr (f a))) = ?x0  apply e0. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x'1 = (isretr (f (g (f a))))^ reflexivity.  } 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x = isretr (f (g (f a))) @ (isretr (f (g (f a))))^
               symmetry. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
isretr (f (g (f a))) @ (isretr (f (g (f a))))^ = ?x  apply inv_inv'. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x'0 = ap (fun b : B => f (g b)) (ap f (issect a)) reflexivity.  } 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
?x' =
eq_refl @ ap (fun b : B => f (g b)) (ap f (issect a))
              reflexivity.  } 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
eq_refl =
ap (fun x : B => f (g x)) (ap f (issect a)^) @
(eq_refl @ ap (fun b : B => f (g b)) (ap f (issect a)))
   repeat rewrite <- ap_compose. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
eq_refl =
ap (fun x : A => f (g (f x))) (issect a)^ @
(eq_refl @ ap (fun x : A => f (g (f x))) (issect a))
   cbn. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
eq_refl =
ap (fun x : A => f (g (f x))) (issect a)^ @
ap (fun x : A => f (g (f x))) (issect a)  symmetry. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
ap (fun x : A => f (g (f x))) (issect a)^ @
ap (fun x : A => f (g (f x))) (issect a) = eq_refl  eapply concat. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
ap (fun x : A => f (g (f x))) (issect a)^ @
ap (fun x : A => f (g (f x))) (issect a) =
?y  refine (ap_pp ((f ∘ g) ∘f) _ _)^. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
ap (f ∘ g) ∘ f ((issect a)^ @ issect a) = eq_refl
   rewrite inv_inv. 
A, B: Type
f: A -> B
g: B -> A
issect: g ∘ f == id
isretr: f ∘ g == id
a: A
e:= concat_pA1 (fun b : B => (isretr b)^)
  (isretr (f a)): (fun b : B => (isretr b)^) (f (g (f a))) @
ap (fun b : B => f (g b)) (isretr (f a)) =
isretr (f a) @ (fun b : B => (isretr b)^) (f a)
e0: ap f (ap g (isretr (f a))) = isretr (f (g (f a)))
ap (fun x : A => f (g (f x))) eq_refl = eq_refl reflexivity.
Defined.

Definition isequiv_adjointify {A B : Type} (f : A -> B) (g : B -> A)
           (issect : g∘ f == id) (isretr : f  ∘ g == id)  : IsEquiv f
  := BuildIsEquiv A B f g (issect' f g issect isretr) isretr
                  (is_adjoint' f g issect isretr).