{A : Type} {a0 a1 a2 : A} : O (a0 = a1) -> O (a1 = a2) -> O (a0 = a2). Proof. intros p q. strip_reflections. exact (to O _ (p @ q)). 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.