{A B C : Type@{i}} `{In O B} {C_inO : In O C} (f : A -> B) (g : B -> C) : g o O_rec (O := O) f == O_rec (O := O) (g o f). Proof. refine (O_indpaths _ _ _); intros x. transitivity (g (f x)). - apply ap. apply O_rec_beta. - symmetry. exact (O_rec_beta (g o f) x). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.BiInv Extensions HProp HFiber NullHomotopy Limits.Pullback. Require Import Homotopy.IdentitySystems. Require Import Colimits.Pushout.