{A B : Type} `{In O A} `{In O B} (f g : A -> B) (e : O_functor f == O_functor g) : f == g. Proof. intros x. refine (ap f (eissect (to O A) x)^ @ _). refine (_ @ ap g (eissect (to O A) x)). transitivity ((to O B)^-1 (O_functor f (to O A x))). + symmetry; apply to_O_inv_natural. + transitivity ((to O B)^-1 (O_functor g (to O A x))). * apply ap, e. * apply to_O_inv_natural. 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.