Welcome to a World of Rocq

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