proposition: Lemma ϕo_ϕ₁_ϕ₂ (f : a ⇒ a) : ϕ∙ i f = (ϕ₂ i (id _ ) □ f) □ ϕ₁ i (id _).
proof: Proof. set (q:=pr2 (pr1 (pr2 (pr1 (pr2 i))))); simpl in q; clearbody q. specialize (q _ f (id _ ) f). set (q':=pr1 q). clearbody q'. simpl in q'. clear q. match goal with | [_ : ?a → _ |- _ ] => assert a end. { apply comp_compose2. apply (@id_right C'). } specialize (q' X). clear X. set (q:= comp_compose2' q'). clearbody q; clear q'. simpl in *. change (ϕ∙ i f) with (ϕ∙ (pr1 i) f). rewrite <- q. clear q. rewrite ϕ₂_is_comp. apply idpath. Qed.
imports: UniMath.Folds.UnicodeNotations UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.UnivalenceAxiom UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.Folds.folds_precat UniMath.Folds.from_precats_to_folds_and_back