(functor_coeq h k p q) o functor_coeq_inverse == idmap. Proof. Open Scope long_path_scope. refine (functor_coeq_sect _ _ _ _ _ _ _ _ (eisretr h) (eisretr k) _ _); intros b. all:rewrite !ap_pp, <- eisadj. all:rewrite <- !ap_compose. all:rewrite (concat_pA1_p (eisretr k) _ _). all:rewrite concat_pV_p. all:rewrite <- (ap_compose (k^-1 o _) k). all:rewrite (ap_compose _ (k o k^-1)). all:rewrite (concat_A1p (eisretr k) (ap _ (eisretr h b)^)). 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.