{X Y Z} (f : X -> Y) (g : Y -> Z) : Trunc_functor (g o f) == Trunc_functor g o Trunc_functor f := O_functor_compose (Tr n) f g.
Require Import Basics Types WildCat.Core WildCat.Universe HFiber. Require Import Modalities.Modality.