{A B C : Type} (f : A -> B) (g : B -> C) `{IsConnMap O _ _ f} `{IsConnMap O _ _ (g o f)} : IsConnMap O g. Proof. apply conn_map_from_extension_elim; intros P ? d. exists (conn_map_elim (g o f) P (d oD f)); intros b. pattern b; refine (conn_map_elim f _ _ b); intros a. exact (conn_map_comp (g o f) P (d oD f) a). 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.