{A B C : Type} (f : A -> B) (g : B -> C) (isconn : IsSurjection (g o f)) : IsSurjection g. Proof. intro c. rapply contr_inhabited_hprop. rapply (Trunc_functor _ (X:= (hfiber (g o f) c))). - intros [a p]. exact (f a; p). - apply center, isconn. Defined.
Require Import Basics Types WildCat.Core WildCat.Universe HFiber. Require Import Modalities.Modality.