functor_coeq_inverse o (functor_coeq h k p q) == idmap. Proof. Open Scope long_path_scope. refine (functor_coeq_sect _ _ _ _ _ _ _ _ (eissect h) (eissect k) _ _); intros b. all:rewrite !concat_p_pp, eisadj, <- ap_V, <- !ap_compose. all:rewrite (ap_compose (_ o h) k^-1). all:rewrite <- !(ap_pp k^-1), !concat_pp_p. 1:rewrite (concat_Ap (fun b => (p b)^) (eissect h b)^). 2:rewrite (concat_Ap (fun b => (q b)^) (eissect h b)^). all:rewrite concat_p_Vp, concat_p_pp. all:rewrite <- (ap_compose (k o _) k^-1), (ap_compose _ (k^-1 o k)). all:rewrite (concat_A1p (eissect k) _). all:rewrite ap_V, concat_pV_p; reflexivity. Close Scope long_path_scope. Qed.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Forall Types.Universe Types.Prod. Require Import Colimits.GraphQuotient.