Welcome to a World of Rocq (original) (raw)

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