fact: Definition f_adjoint_gives_g_adjoint_pointwise (b : B) (f_adjoint_at_gb : fg_id (f (g b)) = f_equal f (gf_id (g b))) : gf_id (g b) = f_equal g (fg_id b) := let precomposed_eq : eq_trans (f_equal (fun a => g (f a)) (f_equal g (fg_id b))) (gf_id (g b)) = eq_trans (f_equal g (f_equal (fun b => f (g b)) (fg_id b))) (f_equal g (fg_id b)) := eq_trans (eq_sym (commute_homotopy_id gf_id (f_equal g (fg_id b)))) (eq_rect (f_equal g (fg_id (f (g b)))) (fun p => eq_trans p _ = _) (eq_trans (eq_trans (eq_sym (eq_trans_map_distr g _ _)) (f_equal (fun p => f_equal g p) (commute_homotopy_id fg_id (fg_id b)))) (eq_trans_map_distr g _ _)) _ (eq_trans (eq_trans (f_equal (fun p => f_equal g p) f_adjoint_at_gb) (f_equal_compose f g _)) (eq_id_comm_r _ gf_id (g b)))) in match fg_id b as p return forall p1 p2, eq_trans (f_equal _ (f_equal g p)) p1 = eq_trans (f_equal g (f_equal _ p)) p2 -> p1 = p2 with eq_refl => fun p1 p2 eq => eq_trans (eq_trans (eq_sym (eq_trans_refl_l _)) eq) (eq_trans_refl_l _) end (gf_id (g b)) (f_equal g (fg_id b)) precomposed_eq.