{A B C : Type} (f : A -> B) (g : B -> C) : (O_functor (g o f)) == (O_functor g) o (O_functor f). Proof. srapply O_indpaths; intros x. refine (to_O_natural (g o f) x @ _). transitivity (O_functor g (to O B (f x))). - symmetry. exact (to_O_natural g (f x)). - apply ap; symmetry. exact (to_O_natural 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.